Changeset 12788

Show
Ignore:
Timestamp:
05.11.2009 20:29:32 (2 weeks ago)
Author:
maeder
Message:

also do not create a local thm link if there is a definition link

Files:
1 modified

Legend:

Unmodified
Added
Removed

  • trunk/Proofs/Global.hs

    r12730 r12788  
    251251      newEdge = (node, target, newEdgeLbl) 
    252252      in case defEdgesToTarget of 
    253       (_, _, dl) : _ | isGlobalDef lbltype 
     253      (_, _, dl) : _ | not isHiding 
    254254             -> (dgraph, addEdgeId proof_basis $ dgl_id dl) 
    255255      _ | node == target && isInc (getRealDGLinkType newEdgeLbl)