src/Pure/Proof/extraction.ML
changeset 22596 d0d2af4db18f
parent 22360 26ead7ed4f4b
child 22662 3e492ba59355
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Apr 04 20:22:32 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Apr 04 23:29:33 2007 +0200
     1.3 @@ -718,12 +718,12 @@
     1.4  
     1.5      fun prep_thm (thm, vs) =
     1.6        let
     1.7 -        val {prop, der = (_, prf), sign, ...} = rep_thm thm;
     1.8 +        val {prop, der = (_, prf), thy, ...} = rep_thm thm;
     1.9          val name = Thm.get_name thm;
    1.10          val _ = name <> "" orelse error "extraction: unnamed theorem";
    1.11          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
    1.12            quote name ^ " has no computational content")
    1.13 -      in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
    1.14 +      in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
    1.15  
    1.16      val defs = Library.foldl (fn (defs, (prf, vs)) =>
    1.17        fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);