src/HOL/Tools/recdef.ML

 *)
 
 signature RECDEF =
 sig
   val get_recdef: theory -> string
-    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
+    -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
   val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   val simp_add: attribute
   val simp_del: attribute
   val cong_add: attribute
   val cong_del: attribute
   val wf_add: attribute
   val wf_del: attribute
   val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
     Attrib.src option -> theory -> theory
-      * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
+      * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
-    theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
+    theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
   val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool ->
     local_theory -> Proof.state

 
 (** global and local recdef data **)
 
 (* theory data *)
 
-type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
+type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
 
 structure GlobalRecdefData = Theory_Data
 (
   type T = recdef_info Symtab.table * hints;
   val empty = (Symtab.empty, mk_hints ([], [], [])): T;

 
     val (cs, ss, congs, wfs) = prep_hints thy hints;
     (*We must remove imp_cong to prevent looping when the induction rule
       is simplified. Many induction rules have nested implications that would
       give rise to looping conditional rewriting.*)
-    val (thy, {rules = rules_idx, induct, tcs}) =
+    val (thy, {lhs, rules = rules_idx, induct, tcs}) =
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
       if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]

       thy
       |> Sign.add_path bname
       |> PureThy.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global Spec_Rules.Equational (tcs, flat rules);
-    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
+      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
+    val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy
       |> put_recdef name result
       |> Sign.parent_path;
   in (thy, result) end;