# HG changeset patch
# User haftmann
# Date 1411578630 -7200
# Node ID fe9de4089345a80b4d712ca6083fe7392d1b0989
# Parent  a379d4531d1a98193006fbd688e0987d2bc7c281
tuned

diff -r a379d4531d1a -r fe9de4089345 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Sep 24 21:00:07 2014 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Sep 24 19:10:30 2014 +0200
@@ -478,7 +478,7 @@
 
 val dummyt = Const ("dummy", dummyT);
 
-fun extract thms thy =
+fun extract thm_vss thy =
   let
     val thy' = add_syntax thy;
     val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
@@ -769,7 +769,7 @@
 
       | extr d vs ts Ts hs _ defs = error "extr: bad proof";
 
-    fun prep_thm (thm, vs) =
+    fun prep_thm vs thm =
       let
         val thy = Thm.theory_of_thm thm;
         val prop = Thm.prop_of thm;
@@ -778,11 +778,11 @@
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
           quote name ^ " has no computational content")
-      in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
+      in Reconstruct.reconstruct_proof thy prop prf end;
 
     val defs =
-      fold (fn (prf, vs) => snd o extr 0 vs [] [] [] prf)
-        (map prep_thm thms) [];
+      fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
+        thm_vss [];
 
     fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
       (case Sign.const_type thy (extr_name s vs) of