1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -243,7 +243,7 @@
     1.4  val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
     1.5  
     1.6  (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
     1.7 -fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
     1.8 +fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (Thm.term_of o the o (parse thy)) f
     1.9    | f_mout thy _ = error "f_mout: not called with formula";
    1.10  
    1.11  
    1.12 @@ -271,9 +271,9 @@
    1.13    | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
    1.14  (*
    1.15  > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
    1.16 -> val (_,t1) = split_dsc_t hs (term_of ct);
    1.17 +> val (_,t1) = split_dsc_t hs (Thm.term_of ct);
    1.18  > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
    1.19 -> val (_,t2) = split_dsc_t hs (term_of ct);
    1.20 +> val (_,t2) = split_dsc_t hs (Thm.term_of ct);
    1.21  > typeless t1 = typeless t2;
    1.22  val it = true : bool
    1.23  *)
    1.24 @@ -388,10 +388,10 @@
    1.25    | has_list_type _ = false;
    1.26  (*
    1.27  > val (SOME ct) = parse thy "lll::real list";
    1.28 -> has_list_type (term_of ct);
    1.29 +> has_list_type (Thm.term_of ct);
    1.30  val it = true : bool
    1.31  > val (SOME ct) = parse thy "[lll::real]";
    1.32 -> has_list_type (term_of ct);
    1.33 +> has_list_type (Thm.term_of ct);
    1.34  val it = false : bool *)
    1.35  
    1.36  fun is_parsed (Syn _) = false
    1.37 @@ -1533,7 +1533,7 @@
    1.38  
    1.39  
    1.40  (*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
    1.41 -	      (((head_of o term_of) given) $ (term_of formal)); WN100819*)
    1.42 +	      (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819*)
    1.43  fun tag_form thy (formal, given) =
    1.44   (let
    1.45      val gf = (head_of given) $ formal;
    1.46 @@ -1557,11 +1557,11 @@
    1.47     find the failing item:
    1.48  > val n = 2;
    1.49  > val tag__form = chktyp (n,formals,givens);
    1.50 -> (type_of o term_of o (nth n)) formals; 
    1.51 -> (type_of o term_of o (nth n)) givens;
    1.52 -> atomty ((term_of o (nth n)) formals);
    1.53 -> atomty ((term_of o (nth n)) givens);
    1.54 -> atomty (term_of tag__form);
    1.55 +> (type_of o Thm.term_of o (nth n)) formals; 
    1.56 +> (type_of o Thm.term_of o (nth n)) givens;
    1.57 +> atomty ((Thm.term_of o (nth n)) formals);
    1.58 +> atomty ((Thm.term_of o (nth n)) givens);
    1.59 +> atomty (Thm.term_of tag__form);
    1.60  > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
    1.61   ##################################################### *)
    1.62  
    1.63 @@ -1582,14 +1582,14 @@
    1.64  val givens = map (the o (parse thy)) given;
    1.65  
    1.66  val tag__forms = chktyps (formals, givens);
    1.67 -map ((atomty) o term_of) tag__forms;
    1.68 +map ((atomty) o Thm.term_of) tag__forms;
    1.69   ##################################################### *)
    1.70  
    1.71  
    1.72  (* check pbltypes, announces one failure a time *)
    1.73  (*fun chk_vars ctppc = 
    1.74    let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} = 
    1.75 -    appc flat (mappc (vars o term_of) ctppc)
    1.76 +    appc flat (mappc (vars o Thm.term_of) ctppc)
    1.77    in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
    1.78       else if (re\\(gi union fi)) <> [] 
    1.79  	    then ("re\\(gi union fi)",re\\(gi union fi))
    1.80 @@ -1632,8 +1632,8 @@
    1.81    in ((fld f) o rev) xs end;
    1.82  (*
    1.83  > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
    1.84 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
    1.85 -> val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
    1.86 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
    1.87 +> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
    1.88  > Thm.global_cterm_of thy conj;
    1.89  val it = "(a = b & c = d) & e = f" : cterm
    1.90  *)
    1.91 @@ -1644,8 +1644,8 @@
    1.92    | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
    1.93  (*
    1.94  > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
    1.95 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
    1.96 -> val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
    1.97 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
    1.98 +> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
    1.99  > Thm.global_cterm_of thy conj;
   1.100  val it = "a = b & c = d & e = f & g = h" : cterm
   1.101  *)