src/Pure/Proof/extraction.ML
changeset 20548 8ef25fe585a8
parent 19482 9f11af8f7ef9
child 20664 ffbc5a57191a
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -277,7 +277,7 @@
     1.4    | freeze T = T;
     1.5  
     1.6  fun freeze_thaw f x =
     1.7 -  map_term_types thaw (f (map_term_types freeze x));
     1.8 +  map_types thaw (f (map_types freeze x));
     1.9  
    1.10  fun etype_of thy vs Ts t =
    1.11    let
    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_term_types thw (term_of (read_cterm thy' (s1, T')));
    1.17 +      val t = map_types thw (term_of (read_cterm thy' (s1, T')));
    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) $