src/HOL/Tools/inductive_codegen.ML

--- a/src/HOL/Tools/inductive_codegen.ML	Thu Feb 25 15:36:38 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Feb 26 09:49:00 2010 +0100
@@ -52,12 +52,13 @@
     fun thyname_of s = (case optmod of
       NONE => Codegen.thyname_of_const thy s | SOME s => s);
   in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
-      SOME (Const ("op =", _), [t, _]) => (case head_of t of
-        Const (s, _) =>
-          CodegenData.put {intros = intros, graph = graph,
-             eqns = eqns |> Symtab.map_default (s, [])
-               (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
-      | _ => (warn thm; thy))
+      SOME (Const (@{const_name "op ="}, _), [t, _]) =>
+        (case head_of t of
+          Const (s, _) =>
+            CodegenData.put {intros = intros, graph = graph,
+               eqns = eqns |> Symtab.map_default (s, [])
+                 (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
+        | _ => (warn thm; thy))
     | SOME (Const (s, _), _) =>
         let
           val cs = fold Term.add_const_names (Thm.prems_of thm) [];
@@ -187,7 +188,7 @@
         end)) (AList.lookup op = modes name)
 
   in (case strip_comb t of
-      (Const ("op =", Type (_, [T, _])), _) =>
+      (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
         [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
         (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
     | (Const (name, _), args) => the_default default (mk_modes name args)
@@ -578,17 +579,20 @@
       fun get_nparms s = if s mem names then SOME nparms else
         Option.map #3 (get_clauses thy s);
 
-      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true)
-        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false)
+      fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
+            Prem ([t], Envir.beta_eta_contract u, true)
+        | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
+            Prem ([t, u], eq, false)
         | dest_prem (_ $ t) =
             (case strip_comb t of
-               (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
-             | (c as Const (s, _), ts) => (case get_nparms s of
-                 NONE => Sidecond t
-               | SOME k =>
-                   let val (ts1, ts2) = chop k ts
-                   in Prem (ts2, list_comb (c, ts1), false) end)
-             | _ => Sidecond t);
+              (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
+            | (c as Const (s, _), ts) =>
+                (case get_nparms s of
+                  NONE => Sidecond t
+                | SOME k =>
+                    let val (ts1, ts2) = chop k ts
+                    in Prem (ts2, list_comb (c, ts1), false) end)
+            | _ => Sidecond t);
 
       fun add_clause intr (clauses, arities) =
         let
@@ -601,7 +605,7 @@
           (AList.update op = (name, these (AList.lookup op = clauses name) @
              [(ts2, prems)]) clauses,
            AList.update op = (name, (map (fn U => (case strip_type U of
-                 (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
+                 (Rs as _ :: _, @{typ bool}) => SOME (length Rs)
                | _ => NONE)) Ts,
              length Us)) arities)
         end;
@@ -633,7 +637,7 @@
     val (ts1, ts2) = chop k ts;
     val u = list_comb (Const (s, T), ts1);
 
-    fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1)
+    fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
       | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
 
     val module' = if_library thyname module;
@@ -716,7 +720,7 @@
   end;
 
 fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
-    (Const ("Collect", _), [u]) =>
+    (Const (@{const_name Collect}, _), [u]) =>
       let val (r, Ts, fs) = HOLogic.strip_psplits u
       in case strip_comb r of
           (Const (s, T), ts) =>