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