# HG changeset patch
# User wenzelm
# Date 1213808104 -7200
# Node ID bcb071683184d8e11a2093751001e04166f4fbc2
# Parent  0ea8e825a1b353a7ee24740885b77676f62e5cfc
added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);

diff -r 0ea8e825a1b3 -r bcb071683184 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Wed Jun 18 18:55:03 2008 +0200
+++ b/src/Pure/old_goals.ML	Wed Jun 18 18:55:04 2008 +0200
@@ -44,6 +44,9 @@
 signature OLD_GOALS =
 sig
   include GOALS
+  val simple_read_term: theory -> typ -> string -> term
+  val read_term: theory -> string -> term
+  val read_prop: theory -> string -> term
   type proof
   val chop: unit -> unit
   val reset_goals: unit -> unit
@@ -66,9 +69,26 @@
 structure OldGoals: OLD_GOALS =
 struct
 
+(* global context *)
+
 val the_context = ML_Context.the_global_context;
 
 
+(* old ways of reading terms *)
+
+fun simple_read_term thy T s =
+  let
+    val ctxt = ProofContext.init thy
+      |> ProofContext.allow_dummies
+      |> ProofContext.set_mode ProofContext.mode_schematic;
+    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
+  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
+
+fun read_term thy = simple_read_term thy dummyT;
+fun read_prop thy = simple_read_term thy propT;
+
+
+
 (*** Goal package ***)
 
 (*Each level of goal stack includes a proof state and alternative states,
@@ -224,9 +244,9 @@
 
 (*Version taking the goal as a string*)
 fun prove_goalw thy rths agoal tacsf =
-  let val chorn = Thm.read_cterm thy (agoal, propT)
+  let val chorn = cterm_of thy (read_prop thy agoal)
   in prove_goalw_cterm_general true rths chorn tacsf end
-  handle ERROR msg => cat_error msg (*from read_cterm?*)
+  handle ERROR msg => cat_error msg (*from read_prop?*)
                 ("The error(s) above occurred for " ^ quote agoal);
 
 (*String version with no meta-rewrite-rules*)
@@ -339,7 +359,7 @@
 
 (*Version taking the goal as a string*)
 fun agoalw atomic thy rths agoal =
-    agoalw_cterm atomic rths (Thm.read_cterm thy (agoal, propT))
+    agoalw_cterm atomic rths (cterm_of thy (read_prop thy agoal))
     handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
         ("The error(s) above occurred for " ^ quote agoal);