diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Jun 20 22:13:59 2005 +0200
@@ -115,7 +115,7 @@
             Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
         in SOME (Envir.norm_term env'' (inc (ren tm2)))
         end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
-          (sort (Int.compare o pairself fst)
+          (sort (int_ord o pairself fst)
             (Net.match_term rules (Pattern.eta_contract tm)))
       end;
 
@@ -774,7 +774,7 @@
     (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 (a, NONE), (vs, s1, s2))) xs) thy)));
+         (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
 
 val realizabilityP =
   OuterSyntax.command "realizability"
@@ -789,7 +789,7 @@
 val extractP =
   OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
     (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
-      (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair NONE)) xs) thy)));
+      (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
 
 val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];