# HG changeset patch
# User wenzelm
# Date 1163459739 -3600
# Node ID 1fb804b96d7cdbf33471680142a93c1ff90476fe
# Parent  6e58289b66853902e04c9bbc7ba73f5512dd1002
recdef_tc(_i): local_theory interface via Specification.theorem_i;
incorporated IsarThy into IsarCmd;

diff -r 6e58289b6685 -r 1fb804b96d7c src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Nov 14 00:15:38 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Tue Nov 14 00:15:39 2006 +0100
@@ -27,8 +27,8 @@
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
     -> theory -> theory * {induct_rules: thm}
-  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
-  val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
+  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> local_theory -> Proof.state
+  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> local_theory -> Proof.state
   val setup: theory -> theory
 end;
 
@@ -272,28 +272,32 @@
       ||> Theory.parent_path;
   in (thy3, {induct_rules = induct_rules'}) end;
 
-val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
-val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
+val defer_recdef = gen_defer_recdef Tfl.defer IsarCmd.apply_theorems;
+val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarCmd.apply_theorems_i;
 
 
 
 (** recdef_tc(_i) **)
 
-fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i thy =
+fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i lthy =
   let
+    val thy = ProofContext.theory_of lthy;
     val name = prep_name thy raw_name;
     val atts = map (prep_att thy) raw_atts;
     val tcs =
       (case get_recdef thy name of
         NONE => error ("No recdef definition of constant: " ^ quote name)
       | SOME {tcs, ...} => tcs);
-    val i = getOpt (opt_i, 1);
-    val tc = List.nth (tcs, i - 1) handle Subscript =>
+    val i = the_default 1 opt_i;
+    val tc = nth tcs (i - 1) handle Subscript =>
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
-  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, []) thy end;
+  in
+    Specification.theorem_i PureThy.internalK NONE (K I) (bname, atts)
+      [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) lthy
+  end;
 
-val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
+val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
 val recdef_tc_i = gen_recdef_tc (K I) (K I);
 
 
@@ -339,9 +343,10 @@
 
 val recdef_tcP =
   OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
-    (P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
-      >> (fn ((thm_name, name), i) =>
-        Toplevel.print o Toplevel.theory_to_proof (recdef_tc thm_name name i)));
+    (P.opt_locale_target --
+      P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+      >> (fn (((loc, thm_name), name), i) =>
+        Toplevel.print o Toplevel.local_theory_to_proof loc (recdef_tc thm_name name i)));
 
 
 val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];