src/Pure/Proof/extraction.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26435 bdce320cd426
--- a/src/Pure/Proof/extraction.ML	Wed Mar 19 22:50:42 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Mar 20 00:20:44 2008 +0100
@@ -765,8 +765,7 @@
   K.thy_decl
     (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
      (fn xs => Toplevel.theory (fn thy => add_realizers
-       (map (fn (((a, vs), s1), s2) =>
-         (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy)));
+       (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
 
 val _ =
   OuterSyntax.command "realizability"
@@ -781,7 +780,7 @@
 val _ =
   OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
     (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
-      extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy)));
+      extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
 
 val etype_of = etype_of o add_syntax;