src/Pure/Proof/extraction.ML
changeset 46219 426ed18eba43
parent 44057 fda143b5c2f5
child 46909 3c73a121a387
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -283,11 +283,14 @@
     1.4      val {typeof_eqns, ...} = ExtractionData.get thy;
     1.5      fun err () = error ("Unable to determine type of extracted program for\n" ^
     1.6        Syntax.string_of_term_global thy t)
     1.7 -  in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
     1.8 -    [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
     1.9 -      Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
    1.10 +  in
    1.11 +    (case
    1.12 +      strip_abs_body
    1.13 +        (freeze_thaw (condrew thy (#net typeof_eqns) [typeof_proc [] vs])
    1.14 +          (fold (Term.abs o pair "x") Ts
    1.15 +            (Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
    1.16        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
    1.17 -    | _ => err ()
    1.18 +    | _ => err ())
    1.19    end;
    1.20  
    1.21  (** realizers for axioms / theorems, together with correctness proofs **)
    1.22 @@ -513,9 +516,10 @@
    1.23      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
    1.24      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
    1.25  
    1.26 -    fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
    1.27 -      (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
    1.28 -        (map (pair "x") (rev Ts), t)));
    1.29 +    fun app_rlz_rews Ts vs t =
    1.30 +      strip_abs (length Ts)
    1.31 +        (freeze_thaw (condrew thy' rrews (procs @ [typroc vs, rlz_proc]))
    1.32 +          (fold (Term.abs o pair "x") Ts t));
    1.33  
    1.34      fun realizes_null vs prop = app_rlz_rews [] vs
    1.35        (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
    1.36 @@ -564,7 +568,7 @@
    1.37                  val u' = (case AList.lookup (op =) types (tname_of T) of
    1.38                      SOME ((_, SOME f)) => f r eT u T
    1.39                    | _ => Const ("realizes", eT --> T --> T) $ r $ u)
    1.40 -              in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
    1.41 +              in app_rlz_rews Ts vs (fold_rev (Term.abs o pair "x") Us' u') end
    1.42            in (defs', corr_prf % SOME u) end
    1.43  
    1.44        | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =