# HG changeset patch
# User haftmann
# Date 1276165442 -7200
# Node ID 8781d80026fc5a6ddf7e263ded702e6fe312889f
# Parent  09467cdfa1985512cdc334572d022033c93794b9
moved inductive_codegen to place where product type is available; tuned structure name

diff -r 09467cdfa198 -r 8781d80026fc src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Jun 10 12:24:01 2010 +0200
+++ b/src/HOL/Inductive.thy	Thu Jun 10 12:24:02 2010 +0200
@@ -9,7 +9,6 @@
 uses
   ("Tools/inductive.ML")
   "Tools/dseq.ML"
-  ("Tools/inductive_codegen.ML")
   "Tools/Datatype/datatype_aux.ML"
   "Tools/Datatype/datatype_prop.ML"
   "Tools/Datatype/datatype_case.ML"
@@ -286,9 +285,6 @@
 use "Tools/old_primrec.ML"
 use "Tools/primrec.ML"
 
-use "Tools/inductive_codegen.ML"
-setup InductiveCodegen.setup
-
 text{* Lambda-abstractions with pattern matching: *}
 
 syntax
diff -r 09467cdfa198 -r 8781d80026fc src/HOL/Library/SML_Quickcheck.thy
--- a/src/HOL/Library/SML_Quickcheck.thy	Thu Jun 10 12:24:01 2010 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy	Thu Jun 10 12:24:02 2010 +0200
@@ -6,7 +6,7 @@
 begin
 
 setup {*
-  InductiveCodegen.quickcheck_setup #>
+  Inductive_Codegen.quickcheck_setup #>
   Quickcheck.add_generator ("SML", Codegen.test_term)
 *}
 
diff -r 09467cdfa198 -r 8781d80026fc src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 10 12:24:01 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 10 12:24:02 2010 +0200
@@ -14,7 +14,7 @@
   val quickcheck_setup : theory -> theory
 end;
 
-structure InductiveCodegen : INDUCTIVE_CODEGEN =
+structure Inductive_Codegen : INDUCTIVE_CODEGEN =
 struct
 
 open Codegen;
@@ -41,7 +41,7 @@
 );
 
 
-fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
+fun warn thm = warning ("Inductive_Codegen: Not a proper clause:\n" ^
   Display.string_of_thm_without_context thm);
 
 fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
@@ -324,7 +324,7 @@
   | distinct_v t nvs = (t, nvs);
 
 fun is_exhaustive (Var _) = true
-  | is_exhaustive (Const ("Pair", _) $ t $ u) =
+  | is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) =
       is_exhaustive t andalso is_exhaustive u
   | is_exhaustive _ = false;
 
@@ -569,7 +569,7 @@
 and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   add_edge_acyclic (hd names, dep) gr handle
     Graph.CYCLES (xs :: _) =>
-      error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs)
+      error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
   | Graph.UNDEF _ =>
     let
       val _ $ u = Logic.strip_imp_concl (hd intrs);
@@ -825,7 +825,7 @@
     val s = "structure TestTerm =\nstruct\n\n" ^
       cat_lines (map snd code) ^
       "\nopen Generated;\n\n" ^ string_of
-        (Pretty.block [str "val () = InductiveCodegen.test_fn :=",
+        (Pretty.block [str "val () = Inductive_Codegen.test_fn :=",
           Pretty.brk 1, str "(fn p =>", Pretty.brk 1,
           str "case Seq.pull (testf p) of", Pretty.brk 1,
           str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
diff -r 09467cdfa198 -r 8781d80026fc src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Jun 10 12:24:01 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Thu Jun 10 12:24:02 2010 +0200
@@ -401,7 +401,7 @@
       else thm
   in map preproc end;
 
-fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE;
+fun code_ind_att optmod = to_pred_att [] #> Inductive_Codegen.add optmod NONE;
 
 
 (**** definition of inductive sets ****)