# HG changeset patch
# User wenzelm
# Date 1213808099 -7200
# Node ID 121991a4884d539caea64584ef6b3feb96ce0346
# Parent  7eef2b1830324c3c1164645ced8334d522cc297a
OldGoals.simple_read_term;

diff -r 7eef2b183032 -r 121991a4884d src/HOL/Modelcheck/mucke_oracle.ML
--- 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 =
diff -r 7eef2b183032 -r 121991a4884d src/HOLCF/IOA/meta_theory/ioa_package.ML
--- 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
 (
diff -r 7eef2b183032 -r 121991a4884d src/Pure/Proof/extraction.ML
--- 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) $
diff -r 7eef2b183032 -r 121991a4884d src/Pure/codegen.ML
--- 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) --