--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Jun 18 18:54:57 2008 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed Jun 18 18:54:59 2008 +0200
@@ -218,7 +218,7 @@
fun deliver_erg sg tl _ [] = [] |
deliver_erg sg tl typ ((c,tyl)::r) = let
val ft = fun_type_of (rev tyl) typ;
- val trm = Sign.simple_read_term sg ft c;
+ val trm = OldGoals.simple_read_term sg ft c;
in
(con_term_list_of trm (arglist_of sg tl tyl))
@(deliver_erg sg tl typ r)
@@ -658,7 +658,7 @@
val arglist = arglist_of sg tl (snd c);
val tty = type_of_term t;
val con_typ = fun_type_of (rev (snd c)) tty;
- val con = Sign.simple_read_term sg con_typ (fst c);
+ val con = OldGoals.simple_read_term sg con_typ (fst c);
in
replace_termlist_with_args sg tl a con arglist t (l1,l2)
end |
@@ -746,7 +746,7 @@
let
val arglist = arglist_of sg tl (snd c);
val con_typ = fun_type_of (rev (snd c)) ty;
- val con = Sign.simple_read_term sg con_typ (fst c);
+ val con = OldGoals.simple_read_term sg con_typ (fst c);
fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
casc_if2 sg tl x con (a::r) ty trm cl =
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Jun 18 18:54:57 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Jun 18 18:54:59 2008 +0200
@@ -132,7 +132,7 @@
(* making a constructor set from a constructor term (of signature) *)
fun constr_set_string thy atyp ctstr =
let
-val trm = Sign.simple_read_term thy atyp ctstr;
+val trm = OldGoals.simple_read_term thy atyp ctstr;
val l = free_vars_of trm
in
if (check_for_constr thy atyp trm) then
@@ -149,7 +149,7 @@
fun hd_of (Const(a,_)) = a |
hd_of (t $ _) = hd_of t |
hd_of _ = raise malformed;
-val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
+val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
in
hd_of trm handle malformed =>
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
@@ -177,8 +177,8 @@
(where bool indicates whether there is a precondition *)
fun extend thy atyp statetupel (actstr,r,[]) =
let
-val trm = Sign.simple_read_term thy atyp actstr;
-val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
+val trm = OldGoals.simple_read_term thy atyp actstr;
+val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm)
@@ -191,8 +191,8 @@
fun pseudo_poststring [] = "" |
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
-val trm = Sign.simple_read_term thy atyp actstr;
-val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
+val trm = OldGoals.simple_read_term thy atyp actstr;
+val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm) then
@@ -364,7 +364,7 @@
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
"_initial, " ^ automaton_name ^ "_trans,{},{})")
])
-val chk_prime_list = (check_free_primed (Sign.simple_read_term thy2 (Type("bool",[]))
+val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
in
(
--- a/src/Pure/Proof/extraction.ML Wed Jun 18 18:54:57 2008 +0200
+++ b/src/Pure/Proof/extraction.ML Wed Jun 18 18:54:59 2008 +0200
@@ -319,7 +319,7 @@
val T = etype_of thy' vs [] prop;
val (T', thw) = Type.freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
- val t = map_types thw (Sign.simple_read_term thy' T' s1);
+ val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
val r' = freeze_thaw (condrew thy' eqns
(procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
--- a/src/Pure/codegen.ML Wed Jun 18 18:54:57 2008 +0200
+++ b/src/Pure/codegen.ML Wed Jun 18 18:54:59 2008 +0200
@@ -890,7 +890,7 @@
end;
val generate_code_i = gen_generate_code Sign.cert_term;
-val generate_code = gen_generate_code Sign.read_term;
+val generate_code = gen_generate_code OldGoals.read_term;
(**** Reflection ****)
@@ -1136,7 +1136,7 @@
P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
(fn xs => Toplevel.theory (fn thy => fold (assoc_const o
(fn ((const, mfx), aux) =>
- (const, (parse_mixfix (Sign.read_term thy) mfx, aux)))) xs thy)));
+ (const, (parse_mixfix (OldGoals.read_term thy) mfx, aux)))) xs thy)));
fun parse_code lib =
Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --