src/HOL/Tools/Sledgehammer/metis_clauses.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39318 ad9a1f9b0558
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  val const_trans_table =
     1.5    Symtab.make [(@{type_name Product_Type.prod}, "prod"),
     1.6                 (@{type_name Sum_Type.sum}, "sum"),
     1.7 -               (@{const_name "op ="}, "equal"),
     1.8 +               (@{const_name HOL.eq}, "equal"),
     1.9                 (@{const_name HOL.conj}, "and"),
    1.10                 (@{const_name HOL.disj}, "or"),
    1.11                 (@{const_name HOL.implies}, "implies"),
    1.12 @@ -111,7 +111,7 @@
    1.13  
    1.14  (* Invert the table of translations between Isabelle and ATPs. *)
    1.15  val const_trans_table_inv =
    1.16 -  Symtab.update ("fequal", @{const_name "op ="})
    1.17 +  Symtab.update ("fequal", @{const_name HOL.eq})
    1.18                  (Symtab.make (map swap (Symtab.dest const_trans_table)))
    1.19  
    1.20  val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
    1.21 @@ -185,8 +185,8 @@
    1.22      SOME c' => c'
    1.23    | NONE => ascii_of c
    1.24  
    1.25 -(* "op =" MUST BE "equal" because it's built into ATPs. *)
    1.26 -fun make_fixed_const @{const_name "op ="} = "equal"
    1.27 +(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
    1.28 +fun make_fixed_const @{const_name HOL.eq} = "equal"
    1.29    | make_fixed_const c = const_prefix ^ lookup_const c
    1.30  
    1.31  fun make_fixed_type_const c = type_const_prefix ^ lookup_const c