1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Tue Jan 11 15:28:03 2011 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Feb 21 19:40:36 2011 +0100
     1.3 @@ -395,7 +395,7 @@
     1.4     identifiers starting with "#" come from Calc and
     1.5     get a hand-made theorem (containing numerals only).*)
     1.6  fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
     1.7 -    (case explode thmid of
     1.8 +    (case Symbol.explode thmid of
     1.9  	"s"::"y"::"m"::"_"::id => 
    1.10  	if hd id = "#" 
    1.11  	then mk_thm thy ct'
    1.12 @@ -407,13 +407,13 @@
    1.13  	     ) handle _ => 
    1.14  		      error ("assoc_thm': '"^thmid^"' not in '"^
    1.15  				   (theory2domID thy)^"' (and parents)");
    1.16 -(*> assoc_thm' (theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
    1.17 +(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
    1.18  val it = "6 = 2 * 3" : thm          
    1.19  
    1.20 -> assoc_thm' (theory "Isac") ("add_0_left","");
    1.21 +> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
    1.22  val it = "0 + ?z = ?z" : thm
    1.23  
    1.24 -> assoc_thm' (theory "Isac") ("sym_real_add_zero_left","");
    1.25 +> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
    1.26  val it = "?t = 0 + ?t"  [.] : thm
    1.27  
    1.28  > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
    1.29 @@ -514,7 +514,7 @@
    1.30      end;
    1.31  (*
    1.32  fun instantiate'' thy' subs ((thmid,ct'):thm') = 
    1.33 -  let val thmid_ = implode ("#"::(explode thmid))  (*see type thm'*)
    1.34 +  let val thmid_ = implode ("#"::(Symbol.explode thmid))  (*see type thm'*)
    1.35    in (thmid_, (string_of_thmI o (read_instantiate subs)) 
    1.36        ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
    1.37  
    1.38 @@ -539,7 +539,7 @@
    1.39  (* instantiate''
    1.40  fun instantiate'' thy' subs ((thmid,ct'):thm') = 
    1.41    let 
    1.42 -    val thmid_ = implode ("#"::(explode thmid));  (*see type thm'*)
    1.43 +    val thmid_ = implode ("#"::(Symbol.explode thmid));  (*see type thm'*)
    1.44      val thy = assoc_thy thy';
    1.45      val typs = map (#T o rep_cterm o the o (parse thy)) 
    1.46        ((snd o split_list) subs);
    1.47 @@ -642,7 +642,7 @@
    1.48  
    1.49  
    1.50  
    1.51 -  rewrite_set_ (theory "Isac") eval_rls false test_rls 
    1.52 +  rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls 
    1.53          ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
    1.54    val xxx = (term_of o the o (parse thy)) 
    1.55  	       "matches (?a = ?b) (x = #0)";
    1.56 @@ -652,7 +652,7 @@
    1.57  
    1.58  
    1.59  
    1.60 -  rewrite_set_ (theory "Isac") eval_rls false eval_rls 
    1.61 +  rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls 
    1.62          ((the o (parse thy)) "contains_root (sqrt #0)");
    1.63  val it = SOME ("True",[]) : (cterm * cterm list) option
    1.64