src/Pure/Proof/extraction.ML
changeset 16486 1a12cdb6ee6b
parent 16458 4c6fd0c01d28
child 16787 b6b6e2faaa41
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Jun 20 22:13:58 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jun 20 22:13:59 2005 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4              Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
     1.5          in SOME (Envir.norm_term env'' (inc (ren tm2)))
     1.6          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
     1.7 -          (sort (Int.compare o pairself fst)
     1.8 +          (sort (int_ord o pairself fst)
     1.9              (Net.match_term rules (Pattern.eta_contract tm)))
    1.10        end;
    1.11  
    1.12 @@ -774,7 +774,7 @@
    1.13      (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
    1.14       (fn xs => Toplevel.theory (fn thy => add_realizers
    1.15         (map (fn (((a, vs), s1), s2) =>
    1.16 -         (PureThy.get_thm thy (a, NONE), (vs, s1, s2))) xs) thy)));
    1.17 +         (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
    1.18  
    1.19  val realizabilityP =
    1.20    OuterSyntax.command "realizability"
    1.21 @@ -789,7 +789,7 @@
    1.22  val extractP =
    1.23    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
    1.24      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
    1.25 -      (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair NONE)) xs) thy)));
    1.26 +      (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
    1.27  
    1.28  val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
    1.29