added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
authorwenzelm
Wed Jun 18 18:55:04 2008 +0200 (2008-06-18)
changeset 27256bcb071683184
parent 27255 0ea8e825a1b3
child 27257 ddc00dbad26b
added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/old_goals.ML	Wed Jun 18 18:55:03 2008 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Wed Jun 18 18:55:04 2008 +0200
     1.3 @@ -44,6 +44,9 @@
     1.4  signature OLD_GOALS =
     1.5  sig
     1.6    include GOALS
     1.7 +  val simple_read_term: theory -> typ -> string -> term
     1.8 +  val read_term: theory -> string -> term
     1.9 +  val read_prop: theory -> string -> term
    1.10    type proof
    1.11    val chop: unit -> unit
    1.12    val reset_goals: unit -> unit
    1.13 @@ -66,9 +69,26 @@
    1.14  structure OldGoals: OLD_GOALS =
    1.15  struct
    1.16  
    1.17 +(* global context *)
    1.18 +
    1.19  val the_context = ML_Context.the_global_context;
    1.20  
    1.21  
    1.22 +(* old ways of reading terms *)
    1.23 +
    1.24 +fun simple_read_term thy T s =
    1.25 +  let
    1.26 +    val ctxt = ProofContext.init thy
    1.27 +      |> ProofContext.allow_dummies
    1.28 +      |> ProofContext.set_mode ProofContext.mode_schematic;
    1.29 +    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    1.30 +  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
    1.31 +
    1.32 +fun read_term thy = simple_read_term thy dummyT;
    1.33 +fun read_prop thy = simple_read_term thy propT;
    1.34 +
    1.35 +
    1.36 +
    1.37  (*** Goal package ***)
    1.38  
    1.39  (*Each level of goal stack includes a proof state and alternative states,
    1.40 @@ -224,9 +244,9 @@
    1.41  
    1.42  (*Version taking the goal as a string*)
    1.43  fun prove_goalw thy rths agoal tacsf =
    1.44 -  let val chorn = Thm.read_cterm thy (agoal, propT)
    1.45 +  let val chorn = cterm_of thy (read_prop thy agoal)
    1.46    in prove_goalw_cterm_general true rths chorn tacsf end
    1.47 -  handle ERROR msg => cat_error msg (*from read_cterm?*)
    1.48 +  handle ERROR msg => cat_error msg (*from read_prop?*)
    1.49                  ("The error(s) above occurred for " ^ quote agoal);
    1.50  
    1.51  (*String version with no meta-rewrite-rules*)
    1.52 @@ -339,7 +359,7 @@
    1.53  
    1.54  (*Version taking the goal as a string*)
    1.55  fun agoalw atomic thy rths agoal =
    1.56 -    agoalw_cterm atomic rths (Thm.read_cterm thy (agoal, propT))
    1.57 +    agoalw_cterm atomic rths (cterm_of thy (read_prop thy agoal))
    1.58      handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
    1.59          ("The error(s) above occurred for " ^ quote agoal);
    1.60