Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Interpret/generate.sml
branchdecompose-isar
changeset 41993 2301fe2b9f9c
parent 41990 99e83a0bea44
child 41994 54d8032d66fb 
     1.1 --- a/src/Tools/isac/Interpret/generate.sml	Sun May 15 11:32:41 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Sun May 15 12:36:29 2011 +0200
     1.3 @@ -260,18 +260,22 @@
     1.4  (*generate 1 ppobj in ptree*)
     1.5  (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
     1.6  fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt = 
     1.7 -    (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
     1.8 -			       (Upblmet,itms2itemppc thy [][]))),
     1.9 -     case p_ of Pbl => update_pbl pt p itmlist
    1.10 -	      | Met => update_met pt p itmlist)
    1.11 +      (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet, itms2itemppc thy [][]))),
    1.12 +         case p_ of
    1.13 +           Pbl => update_pbl pt p itmlist
    1.14 +	       | Met => update_met pt p itmlist)
    1.15 +
    1.16    | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt = 
    1.17 -    (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
    1.18 -     case p_ of Pbl => update_pbl pt p itmlist
    1.19 -	      | Met => update_met pt p itmlist)
    1.20 +      (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
    1.21 +         case p_ of
    1.22 +           Pbl => update_pbl pt p itmlist
    1.23 +	       | Met => update_met pt p itmlist)
    1.24 +
    1.25    | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt = 
    1.26 -    (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
    1.27 -     case p_ of Pbl => update_pbl pt p itmlist
    1.28 -	      | Met => update_met pt p itmlist)
    1.29 +      (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
    1.30 +         case p_ of
    1.31 +           Pbl => update_pbl pt p itmlist
    1.32 +	       | Met => update_met pt p itmlist)
    1.33  
    1.34    | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt = 
    1.35      (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
wneuper/isa