1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Mon Oct 11 14:22:50 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Oct 28 09:24:47 2010 +0200
     1.3 @@ -351,13 +351,13 @@
     1.4  
     1.5  (**.set up isab_thm_thy in Isac.ML.**)
     1.6  
     1.7 -fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));
     1.8 -fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));
     1.9 +fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, prop_of thm));
    1.10 +fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term));
    1.11  
    1.12  (*.lookup the missing theorems in some thy (of Isabelle).*)
    1.13  fun make_isa missthms thy =
    1.14      map (pair (theory2thyID thy)) 
    1.15 -	((inter eq_thmI) missthms (PureThy.all_thms_of thy))
    1.16 +	((inter eq_thmI) missthms [] (*PureThy.all_thms_of thy*)) 
    1.17  	: (thyID * (thmID * Thm.thm)) list;
    1.18  
    1.19  (*.separate handling of sym_thms.*)
    1.20 @@ -375,14 +375,15 @@
    1.21  			    ((apsnd o apsnd) sym_thm)) symsym_isab
    1.22  		       
    1.23  	val isab = notsym_isab @ symsym_isab @ sym_isab
    1.24 -    in ((map rearrange) o (gen_sort les)) isab 
    1.25 -       : (thmID * (thyID * Thm.thm)) list
    1.26 +    in ((map rearrange) o (gen_sort les)) isab : (thmID * (thyID * term)) list
    1.27      end;
    1.28 +(*
    1.29  (* version with term instead of thm, for Theory.axioms_of in isa02*)
    1.30  fun make_isa missthms thy =
    1.31      map (pair (theory2thyID thy)) 
    1.32  	((inter eq_thmI') missthms (Theory.axioms_of thy))
    1.33  	: (thyID * (thmID * term)) list;
    1.34 +(* separate handling of sym_thms *)
    1.35  fun make_isab rlsthmsNOTisac isab_thys = 
    1.36      let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
    1.37  	val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
    1.38 @@ -400,6 +401,7 @@
    1.39      in ((map rearrange) o (gen_sort les)) isab 
    1.40         : (thmID * (thyID * term)) list
    1.41      end;
    1.42 +*)
    1.43  
    1.44  (*.which theory below thy' contains a theorem; this can be in isabelle !
    1.45  get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)