src/Pure/Proof/extraction.ML
changeset 22675 acf10be7dcca
parent 22662 3e492ba59355
child 22717 74dbc7696083
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Apr 14 11:05:12 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 14 17:35:52 2007 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  fun read_condeq thy =
     1.5    let val thy' = add_syntax thy
     1.6    in fn s =>
     1.7 -    let val t = Logic.varify (term_of (read_cterm thy' (s, propT)))
     1.8 +    let val t = Logic.varify (Sign.read_prop thy' s)
     1.9      in (map Logic.dest_equals (Logic.strip_imp_prems t),
    1.10        Logic.dest_equals (Logic.strip_imp_concl t))
    1.11      end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
    1.12 @@ -324,7 +324,7 @@
    1.13        val T = etype_of thy' vs [] prop;
    1.14        val (T', thw) = Type.freeze_thaw_type
    1.15          (if T = nullT then nullT else map fastype_of vars' ---> T);
    1.16 -      val t = map_types thw (term_of (read_cterm thy' (s1, T')));
    1.17 +      val t = map_types thw (Sign.simple_read_term thy' T' s1);
    1.18        val r' = freeze_thaw (condrew thy' eqns
    1.19          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
    1.20            (Const ("realizes", T --> propT --> propT) $