1.1 --- a/src/Tools/isac/Interpret/appl.sml Mon Dec 07 10:01:49 2015 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Dec 07 10:17:08 2015 +0100
1.3 @@ -60,11 +60,11 @@
1.4 end;
1.5
1.6 val op_and = Const ("op &", [bool, bool] ---> bool);
1.7 -(*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
1.8 +(*> (Thm.global_cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
1.9 val it = "a & b" : cterm
1.10 *)
1.11 fun mk_and a b = op_and $ a $ b;
1.12 -(*> (cterm_of thy)
1.13 +(*> (Thm.global_cterm_of thy)
1.14 (mk_and (Free("a",bool)) (Free("b",bool)));
1.15 val it = "a & b" : cterm*)
1.16
1.17 @@ -76,7 +76,7 @@
1.18 in mk t ts end;
1.19 (*> val pred = map (term_of o the o (parse thy))
1.20 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
1.21 -> (cterm_of thy) (mk_and pred);
1.22 +> (Thm.global_cterm_of thy) (mk_and pred);
1.23 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
1.24
1.25
1.26 @@ -177,7 +177,7 @@
1.27 > val pred = (term_of o the o (parse thy))
1.28 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
1.29 > val ttt = check_elementwise thy consts (bdv, pred);
1.30 -> (cterm_of thy) ttt;
1.31 +> (Thm.global_cterm_of thy) ttt;
1.32 val it = "[x = #-3, x = #3]" : cterm
1.33
1.34 > val consts = (term_of o the o (parse thy)) "[x = #4]";
1.35 @@ -185,7 +185,7 @@
1.36 > val pred = (term_of o the o (parse thy))
1.37 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
1.38 > val ttt = check_elementwise thy consts (bdv,pred);
1.39 -> (cterm_of thy) ttt;
1.40 +> (Thm.global_cterm_of thy) ttt;
1.41 val it = "[x = #4]" : cterm
1.42
1.43 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
1.44 @@ -193,7 +193,7 @@
1.45 > val pred = (term_of o the o (parse thy))
1.46 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
1.47 > val ttt = check_elementwise thy consts (bdv,pred);
1.48 -> (cterm_of thy) ttt;
1.49 +> (Thm.global_cterm_of thy) ttt;
1.50 val it = "[]" : cterm*)
1.51
1.52
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Dec 07 10:01:49 2015 +0100
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Dec 07 10:17:08 2015 +0100
2.3 @@ -812,7 +812,7 @@
2.4 (* val (thy, (str, (dsc, _)), (ty $ var)) =
2.5 (thy, p, a);
2.6 *)
2.7 - (cterm_of thy (dsc $ var);(*type check*)
2.8 + (Thm.global_cterm_of thy (dsc $ var);(*type check*)
2.9 SOME ((([1], str, dsc, (*[var]*)
2.10 split_dts' (dsc, var))): preori)(*:ori without leading #*))
2.11 handle e as TYPE _ =>
2.12 @@ -1532,12 +1532,12 @@
2.13 in f end;
2.14
2.15
2.16 -(*fun tag_form thy (formal, given) = cterm_of thy
2.17 +(*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
2.18 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
2.19 fun tag_form thy (formal, given) =
2.20 (let
2.21 val gf = (head_of given) $ formal;
2.22 - val _ = cterm_of thy gf
2.23 + val _ = Thm.global_cterm_of thy gf
2.24 in gf end)
2.25 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
2.26 " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
2.27 @@ -1632,9 +1632,9 @@
2.28 in ((fld f) o rev) xs end;
2.29 (*
2.30 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
2.31 -> val ces = map (cterm_of thy) (isalist2list (term_of ct));
2.32 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
2.33 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
2.34 -> cterm_of thy conj;
2.35 +> Thm.global_cterm_of thy conj;
2.36 val it = "(a = b & c = d) & e = f" : cterm
2.37 *)
2.38
2.39 @@ -1644,9 +1644,9 @@
2.40 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
2.41 (*
2.42 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
2.43 -> val ces = map (cterm_of thy) (isalist2list (term_of ct));
2.44 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
2.45 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
2.46 -> cterm_of thy conj;
2.47 +> Thm.global_cterm_of thy conj;
2.48 val it = "a = b & c = d & e = f & g = h" : cterm
2.49 *)
2.50
3.1 --- a/src/Tools/isac/Interpret/mstools.sml Mon Dec 07 10:01:49 2015 +0100
3.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Dec 07 10:17:08 2015 +0100
3.3 @@ -205,14 +205,14 @@
3.4 typecheck thus may lead to TYPE-error 'unknown constant';
3.5 solution: typecheck with (Thy_Info.get_theory "Isac"); i.e. arg 'thy' superfluous*)
3.6 (*fun comp_dts thy (d,[]) =
3.7 - cterm_of (*(sign_of o assoc_thy) "Isac"*)
3.8 + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)
3.9 (Thy_Info.get_theory "Isac")
3.10 (*comp_dts:FIXXME stay with term for efficiency !!!*)
3.11 (if is_reall_dsc d then (d $ e_listReal)
3.12 else if is_booll_dsc d then (d $ e_listBool)
3.13 else d)
3.14 | comp_dts (d,ts) =
3.15 - (cterm_of (*(sign_of o assoc_thy) "Isac"*)
3.16 + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)
3.17 (Thy_Info.get_theory "Isac")
3.18 (*comp_dts:FIXXME stay with term for efficiency !!*)
3.19 (d $ (comp_ts (d, ts)))
4.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 07 10:01:49 2015 +0100
4.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Dec 07 10:17:08 2015 +0100
4.3 @@ -682,7 +682,7 @@
4.4 *)
4.5
4.6 fun make_rule thy t =
4.7 - let val ct = cterm_of thy (Trueprop $ t)
4.8 + let val ct = Thm.global_cterm_of thy (Trueprop $ t)
4.9 in Thm (term_to_string''' thy (term_of ct), make_thm ct) end;
4.10
4.11 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
5.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Mon Dec 07 10:01:49 2015 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Mon Dec 07 10:17:08 2015 +0100
5.3 @@ -137,11 +137,11 @@
5.4 val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
5.5 val eT = HOLogic.realT;
5.6 val t = mk_mono cT vT pT eT ~5 "x" 5;
5.7 -(cterm_of thy) t;
5.8 +(Thm.global_cterm_of thy) t;
5.9 val t = mk_mono cT vT pT eT ~1 "x" 0;
5.10 -(cterm_of thy) t;
5.11 +(Thm.global_cterm_of thy) t;
5.12 val t = mk_mono cT vT pT eT 1 "x" 1;
5.13 -(cterm_of thy) t;
5.14 +(Thm.global_cterm_of thy) t;
5.15
5.16
5.17 fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
5.18 @@ -164,21 +164,21 @@
5.19
5.20 (*tests*)
5.21 val t = poly2term cT vT pT eT [~1] "x";
5.22 -(cterm_of thy) t;
5.23 +(Thm.global_cterm_of thy) t;
5.24 val t = poly2term cT vT pT eT [0,1] "x";
5.25 -(cterm_of thy) t;
5.26 +(Thm.global_cterm_of thy) t;
5.27 val t = poly2term cT vT pT eT [0,0,0,1] "x";
5.28 -(cterm_of thy) t;
5.29 +(Thm.global_cterm_of thy) t;
5.30 val t = poly2term cT vT pT eT [0,0,0,3] "x";
5.31 -(cterm_of thy) t;
5.32 +(Thm.global_cterm_of thy) t;
5.33 val t = poly2term cT vT pT eT [~1,0,0,3] "x";
5.34 -(cterm_of thy) t;
5.35 +(Thm.global_cterm_of thy) t;
5.36 val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
5.37 -(cterm_of thy) t;
5.38 +(Thm.global_cterm_of thy) t;
5.39 val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
5.40 -(cterm_of thy) t;
5.41 +(Thm.global_cterm_of thy) t;
5.42 val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
5.43 -(cterm_of thy) t;
5.44 +(Thm.global_cterm_of thy) t;
5.45
5.46 "***************************************************************************";
5.47 "* reverse-rewriting 12.8.02 *";
6.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Dec 07 10:01:49 2015 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Dec 07 10:17:08 2015 +0100
6.3 @@ -747,7 +747,7 @@
6.4 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
6.5 "(matches ( v_v ^^^2 = 0, e_e::bool))";
6.6 val prei = subst_atomic env pre;
6.7 - val cpre = (cterm_of thy) prei;
6.8 + val cpre = (Thm.global_cterm_of thy) prei;
6.9
6.10 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
6.11 val ct = "True | False | False | False" : cterm
7.1 --- a/src/Tools/isac/ProgLang/Tools.sml Mon Dec 07 10:01:49 2015 +0100
7.2 +++ b/src/Tools/isac/ProgLang/Tools.sml Mon Dec 07 10:17:08 2015 +0100
7.3 @@ -46,7 +46,7 @@
7.4 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
7.5 \else hd [A = a * b, a // #2 = #2]";
7.6
7.7 -> (cterm_of thy) t';
7.8 +> (Thm.global_cterm_of thy) t';
7.9 > val t = (term_of o the o (parse thy)) s;
7.10 > val eval_fn = the (assoc (!eval_list, op_));
7.11 > val (SOME(_,t')) = get_pair op_ eval_fn t;
7.12 @@ -92,7 +92,7 @@
7.13
7.14 > val eval_fn = the (assoc (!eval_list, op_));
7.15 > val (SOME(id,t')) = get_pair op_ eval_fn t;
7.16 -> (cterm_of thy) t';
7.17 +> (Thm.global_cterm_of thy) t';
7.18 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
7.19 *)
7.20
8.1 --- a/src/Tools/isac/ProgLang/calculate.sml Mon Dec 07 10:01:49 2015 +0100
8.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Mon Dec 07 10:17:08 2015 +0100
8.3 @@ -192,7 +192,7 @@
8.4 NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_);
8.5 tracing ("@@@ get_calculation: ct= "); atomty ct; *)
8.6 NONE)
8.7 - | SOME (thmid, t) => SOME (thmid, (make_thm o (cterm_of thy)) t);
8.8 + | SOME (thmid, t) => SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t);
8.9 (*
8.10 > val ct = (the o (parse thy)) "#9 is_const";
8.11 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
8.12 @@ -307,7 +307,7 @@
8.13 case eval_fn op_ ct thy of
8.14 NONE => NONE
8.15 | SOME (thmid,t) =>
8.16 - SOME (thmid, (make_thm o (cterm_of thy)) t);
8.17 + SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t);
8.18
8.19
8.20
9.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 10:01:49 2015 +0100
9.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 10:17:08 2015 +0100
9.3 @@ -323,7 +323,7 @@
9.4 val t' = case t of
9.5 Const ("==>",_) $ _ $ _ => t
9.6 | _ => Trueprop $ t
9.7 - in make_thm (cterm_of thy t') end;
9.8 + in make_thm (Thm.global_cterm_of thy t') end;
9.9 (*
9.10 val str = "?r ^^^ 2 = ?r * ?r";
9.11 val thm = realpow_twoI;
9.12 @@ -355,7 +355,7 @@
9.13 (*prints subgoal etc.
9.14 ((goal thy);(topthm()) o ) str; *)
9.15 (*assume rejects scheme variables
9.16 - assume ((cterm_of thy) (Trueprop $
9.17 + assume ((Thm.global_cterm_of thy) (Trueprop $
9.18 (term_of o the o (parse thy)) str)); *)
9.19
9.20
10.1 --- a/src/Tools/isac/ProgLang/termC.sml Mon Dec 07 10:01:49 2015 +0100
10.2 +++ b/src/Tools/isac/ProgLang/termC.sml Mon Dec 07 10:17:08 2015 +0100
10.3 @@ -6,7 +6,7 @@
10.4 fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
10.5
10.6 (*
10.7 -> (cterm_of thy) a_term;
10.8 +> (Thm.global_cterm_of thy) a_term;
10.9 val it = "empty" : cterm *)
10.10
10.11 (*2003 fun match thy t pat =
10.12 @@ -295,7 +295,7 @@
10.13 > val tt = (term_of o the o (parse thy)) "R=(R::real)";
10.14 > val TT = type_of tt;
10.15 > val ss = list2isalist TT [tt,tt,tt];
10.16 -> (cterm_of thy) ss;
10.17 +> (Thm.global_cterm_of thy) ss;
10.18 val it = "[R = R, R = R, R = R]" : cterm *)
10.19
10.20 fun isapair2pair (Const ("Product_Type.Pair",_) $ a $ b) = (a,b)
10.21 @@ -326,8 +326,8 @@
10.22 val bool = Type ("HOL.bool",[]); (* 2002 Integ.int *)
10.23 val Trueprop = HOLogic.Trueprop;
10.24 fun mk_prop t = HOLogic.mk_Trueprop t;
10.25 -val true_as_cterm = cterm_of (Thy_Info.get_theory "HOL") @{term True};
10.26 -val false_as_cterm = cterm_of (Thy_Info.get_theory "HOL") @{term False};
10.27 +val true_as_cterm = Thm.global_cterm_of (Thy_Info.get_theory "HOL") @{term True};
10.28 +val false_as_cterm = Thm.global_cterm_of (Thy_Info.get_theory "HOL") @{term False};
10.29
10.30 infixr 5 -->; (*2002 /Pure/term.ML *)
10.31 infixr --->; (*2002 /Pure/term.ML *)
10.32 @@ -604,7 +604,7 @@
10.33 (*
10.34 val T = (type_of o term_of o the) (parse thy "#12::real");
10.35 val t = mk_factroot "SqRoot.sqrt" T 2 3;
10.36 -(cterm_of thy) t;
10.37 +(Thm.global_cterm_of thy) t;
10.38 val it = "#2 * sqrt #3 " : cterm
10.39 *)
10.40 fun var_op_num v op_ optype ntyp n =
10.41 @@ -621,7 +621,7 @@
10.42 (*
10.43 > val t = num_op_num "Int" 3 4;
10.44 > atomty t;
10.45 -> string_of_cterm ((cterm_of thy) t);
10.46 +> string_of_cterm ((Thm.global_cterm_of thy) t);
10.47 *)
10.48
10.49
10.50 @@ -800,7 +800,7 @@
10.51 atomty t; (* 'a *)
10.52 val t' = set_types al t;
10.53 atomty t'; (*real*)
10.54 -(cterm_of thy) t';
10.55 +(Thm.global_cterm_of thy) t';
10.56 val it = "x = #0 + #-1 * #-4" : cterm
10.57
10.58 val t = (term_of o the o (parse thy))
10.59 @@ -808,7 +808,7 @@
10.60 atomty t;
10.61 val t' = set_types al t;
10.62 atomty t';
10.63 -(cterm_of thy) t';
10.64 +(Thm.global_cterm_of thy) t';
10.65 uncaught exception TYPE (*^^^ is new, NOT in al*)
10.66 *)
10.67
10.68 @@ -1042,35 +1042,35 @@
10.69 fun parseold thy str =
10.70 (let val t = ((*typ_a2real o*) numbers_to_string)
10.71 (Syntax.read_term_global thy str)
10.72 - in SOME (cterm_of thy t) end)
10.73 + in SOME (Thm.global_cterm_of thy t) end)
10.74 handle _ => NONE;
10.75 (*2002 fun parseN thy str =
10.76 (let
10.77 val sgn = sign_of thy;
10.78 val t = ((*typ_a2real o app_num_tr'1 o*) term_of)
10.79 (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
10.80 - in SOME (cterm_of sgn t) end)
10.81 + in SOME (Thm.global_cterm_of sgn t) end)
10.82 handle _ => NONE;*)
10.83 fun parseN thy str =
10.84 (let val t = (*(typ_a2real o numbers_to_string)*)
10.85 (Syntax.read_term_global thy str)
10.86 - in SOME (cterm_of thy t) end)
10.87 + in SOME (Thm.global_cterm_of thy t) end)
10.88 handle _ => NONE;
10.89 (*2002 fun parse thy str =
10.90 (let
10.91 val sgn = sign_of thy;
10.92 val t = (typ_a2real o app_num_tr'1 o term_of)
10.93 (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
10.94 - in SOME (cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
10.95 + in SOME (Thm.global_cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
10.96 handle _ => NONE;*)
10.97 (*2010 fun parse thy str =
10.98 (let val t = (typ_a2real o app_num_tr'1) (Syntax.read_term_global thy str)
10.99 - in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
10.100 + in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
10.101 handle _ => NONE;*)
10.102 fun parse thy str =
10.103 (let val t = (typ_a2real o numbers_to_string)
10.104 (Syntax.read_term_global thy str)
10.105 - in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
10.106 + in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
10.107 handle _ => NONE;
10.108 (*
10.109 > val (SOME ct) = parse thy "(-#5)^^^#3";