# HG changeset patch
# User wenzelm
# Date 1266530911 -3600
# Node ID 48721d3d77e7b6c32399cf1839e30b34ac96fa24
# Parent  c2ddb93954363126e8c44cad53d6c581df2bc20b
typedef: slightly more precise treatment of binding;
tuned;

diff -r c2ddb9395436 -r 48721d3d77e7 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Feb 18 21:26:40 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Thu Feb 18 23:08:31 2010 +0100
@@ -14,10 +14,10 @@
     Rep_induct: thm, Abs_induct: thm}
   val add_typedef: bool -> binding option -> binding * string list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
-  val typedef: (bool * binding) * (binding * string list * mixfix) * term
-    * (binding * binding) option -> theory -> Proof.state
-  val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
-    * (binding * binding) option -> theory -> Proof.state
+  val typedef: (bool * binding) * (binding * string list * mixfix) * term *
+    (binding * binding) option -> theory -> Proof.state
+  val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string *
+    (binding * binding) option -> theory -> Proof.state
   val get_info: theory -> string -> info option
   val the_info: theory -> string -> info
   val interpretation: (string -> theory -> theory) -> theory -> theory
@@ -118,9 +118,9 @@
     fun add_def theory =
       if def then
         theory
-        |> Sign.add_consts_i [(name, setT', NoSyn)]
-        |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
-            (Primitive_Defs.mk_defpair (setC, set)))]
+        |> Sign.add_consts_i [(name, setT', NoSyn)]   (* FIXME authentic syntax *)
+        |> PureThy.add_defs false
+          [((Binding.map_name Thm.def_name name, Logic.mk_equals (setC, set)), [])]
         |-> (fn [th] => pair (SOME th))
       else (NONE, theory);
     fun contract_def NONE th = th
@@ -164,7 +164,7 @@
                   [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
                 ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
                   [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
-            ||> Sign.parent_path;
+            ||> Sign.restore_naming thy1;
           val info = {rep_type = oldT, abs_type = newT,
             Rep_name = full Rep_name, Abs_name = full Abs_name,
               inhabited = inhabited, type_definition = type_definition, set_def = set_def,
@@ -250,24 +250,20 @@
 
 val _ = OuterKeyword.keyword "morphisms";
 
-val typedef_decl =
-  Scan.optional (P.$$$ "(" |--
-      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
-        --| P.$$$ ")") (true, NONE) --
-    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
-    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
-
-fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
-  typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs);
-
 val _ =
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
     OuterKeyword.thy_goal
-    (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
+    (Scan.optional (P.$$$ "(" |--
+        ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
+          P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
+      (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
+    >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
+        Toplevel.print o Toplevel.theory_to_proof
+          (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs))));
 
 end;
 
-
 val setup = Typedef_Interpretation.init;
 
 end;