# HG changeset patch
# User wenzelm
# Date 1256818898 -3600
# Node ID 1e1210f31207aa05045817e3bfce8725b31dbb59
# Parent  a2fa943052547fcd0b14e571061fe4cf31532cbe
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;

diff -r a2fa94305254 -r 1e1210f31207 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 12:59:25 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 13:21:38 2009 +0100
@@ -63,9 +63,11 @@
 
 val get_all = #types o DatatypesData.get;
 val get_info = Symtab.lookup o get_all;
-fun the_info thy name = (case get_info thy name of
-      SOME info => info
-    | NONE => error ("Unknown datatype " ^ quote name));
+
+fun the_info thy name =
+  (case get_info thy name of
+    SOME info => info
+  | NONE => error ("Unknown datatype " ^ quote name));
 
 fun info_of_constr thy (c, T) =
   let
@@ -319,7 +321,7 @@
       [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
     val unnamed_rules = map (fn induct =>
-      ((Binding.empty, [induct]), [Thm.kind_internal, Induct.induct_type ""]))
+      ((Binding.empty, [induct]), [RuleCases.inner_rule, Induct.induct_type ""]))
         (Library.drop (length dt_names, inducts));
   in
     thy9
diff -r a2fa94305254 -r 1e1210f31207 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Oct 29 12:59:25 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Oct 29 13:21:38 2009 +0100
@@ -37,6 +37,8 @@
   val name: string list -> thm -> thm
   val case_names: string list -> attribute
   val case_conclusion: string * string list -> attribute
+  val is_inner_rule: thm -> bool
+  val inner_rule: attribute
   val save: thm -> thm -> thm
   val get: thm -> (string * string list) list * int
   val rename_params: string list list -> thm -> thm
@@ -90,7 +92,7 @@
 
 fun extract_case is_open thy (case_outline, raw_prop) name concls =
   let
-    val rename = if is_open then I else (apfst (Name.internal o Name.clean));
+    val rename = if is_open then I else apfst (Name.internal o Name.clean);
 
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
     val len = length props;
@@ -212,7 +214,7 @@
 val consumes_tagN = "consumes";
 
 fun lookup_consumes th =
-  (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
+  (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
     NONE => NONE
   | SOME s =>
       (case Lexicon.read_nat s of SOME n => SOME n
@@ -223,14 +225,13 @@
 fun put_consumes NONE th = th
   | put_consumes (SOME n) th = th
       |> Thm.untag_rule consumes_tagN
-      |> Thm.tag_rule
-        (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n));
+      |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
 
 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
 
 val save_consumes = put_consumes o lookup_consumes;
 
-fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
+fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
 
 fun consumes_default n x =
   if is_some (lookup_consumes (#2 x)) then x else consumes n x;
@@ -282,7 +283,24 @@
       else NONE)
   in fold add_case_concl concls end;
 
-fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
+fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
+
+
+
+(** inner rule **)
+
+val inner_rule_tagN = "inner_rule";
+
+fun is_inner_rule th =
+  AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
+
+fun put_inner_rule inner =
+  Thm.untag_rule inner_rule_tagN
+  #> inner ? Thm.tag_rule (inner_rule_tagN, "");
+
+val save_inner_rule = put_inner_rule o is_inner_rule;
+
+val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
 
 
 
@@ -290,7 +308,11 @@
 
 (* access hints *)
 
-fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
+fun save th =
+  save_consumes th #>
+  save_case_names th #>
+  save_case_concls th #>
+  save_inner_rule th;
 
 fun get th =
   let
@@ -357,5 +379,5 @@
 
 end;
 
-structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
-open BasicRuleCases;
+structure Basic_Rule_Cases: BASIC_RULE_CASES = RuleCases;
+open Basic_Rule_Cases;
diff -r a2fa94305254 -r 1e1210f31207 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Oct 29 12:59:25 2009 +0100
+++ b/src/Tools/induct.ML	Thu Oct 29 13:21:38 2009 +0100
@@ -570,7 +570,7 @@
       ((fn [] => NONE | ts => List.last ts) #>
         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
         find_inductT ctxt)) [[]]
-  |> filter_out (forall Thm.is_internal);
+  |> filter_out (forall RuleCases.is_inner_rule);
 
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];