# HG changeset patch
# User blanchet
# Date 1410210258 -7200
# Node ID 1c5bc387bd4c791f7d9c6c28f28e58008a147c32
# Parent  a701907d621eaa0cee6fc60a1ff3c795b7d02f75
added flag to 'typedef' to allow concealed definitions

diff -r a701907d621e -r 1c5bc387bd4c src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -168,7 +168,7 @@
   let
     val name = #1 typ
     val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
-      |> Typedef.add_typedef_global typ set opt_morphs tac
+      |> Typedef.add_typedef_global false typ set opt_morphs tac
     val oldT = #rep_type (#1 info)
     val newT = #abs_type (#1 info)
     val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Import/import_rule.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -221,7 +221,7 @@
     val tfrees = Term.add_tfrees c []
     val tnames = sort_strings (map fst tfrees)
     val ((_, typedef_info), thy') =
-     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
+     Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
        (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy
     val aty = #abs_type (#1 typedef_info)
     val th = freezeT (#type_definition (#2 typedef_info))
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -574,7 +574,7 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
-          Typedef.add_typedef_global
+          Typedef.add_typedef_global false
             (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
             (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -324,7 +324,7 @@
     val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Typedef.add_typedef (b', Ts, mx) set opt_morphs tac
+      |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
       ||> `Local_Theory.restore;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -186,7 +186,7 @@
       |> Sign.parent_path
       |> fold_map
         (fn (((name, mx), tvs), c) =>
-          Typedef.add_typedef_global (name, tvs, mx)
+          Typedef.add_typedef_global false (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -45,7 +45,7 @@
     val typedef_tac =
       EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
   in
-    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
+    Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
       (typedef_term rel rty lthy) NONE typedef_tac lthy
   end
 
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/record.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -111,7 +111,7 @@
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
+    |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
         (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -16,10 +16,9 @@
   val get_info: Proof.context -> string -> info list
   val get_info_global: theory -> string -> info list
   val interpretation: (string -> theory -> theory) -> theory -> theory
-  val setup: theory -> theory
-  val add_typedef: binding * (string * sort) list * mixfix ->
+  val add_typedef: bool -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
-  val add_typedef_global: binding * (string * sort) list * mixfix ->
+  val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
   val typedef: (binding * (string * sort) list * mixfix) * term *
     (binding * binding) option -> local_theory -> Proof.state
@@ -83,7 +82,7 @@
 
 fun interpretation f = Typedef_Interpretation.interpretation (with_repaired_path f);
 
-val setup = Typedef_Interpretation.init;
+val _ = Theory.setup Typedef_Interpretation.init;
 
 
 (* primitive typedef axiomatization -- for fresh typedecl *)
@@ -136,8 +135,9 @@
 
 (* prepare_typedef *)
 
-fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
+fun prepare_typedef conceal prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
   let
+    val concealed_name = name |> conceal ? Binding.conceal;
     val bname = Binding.name_of name;
 
 
@@ -169,10 +169,11 @@
 
     val (Rep_name, Abs_name) =
       (case opt_morphs of
-        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+        NONE => (Binding.prefix_name "Rep_" concealed_name,
+          Binding.prefix_name "Abs_" concealed_name)
       | SOME morphs => morphs);
 
-    val typedef_name = Binding.prefix_name "type_definition_" name;
+    val typedef_name = Binding.prefix_name "type_definition_" concealed_name;
 
     val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
       |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set;
@@ -239,18 +240,18 @@
 
 (* add_typedef: tactic interface *)
 
-fun add_typedef typ set opt_morphs tac lthy =
+fun add_typedef conceal typ set opt_morphs tac lthy =
   let
     val ((goal, _, typedef_result), lthy') =
-      prepare_typedef Syntax.check_term typ set opt_morphs lthy;
+      prepare_typedef conceal Syntax.check_term typ set opt_morphs lthy;
     val inhabited =
       Goal.prove lthy' [] [] goal (K tac)
       |> Goal.norm_result lthy' |> Thm.close_derivation;
   in typedef_result inhabited lthy' end;
 
-fun add_typedef_global typ set opt_morphs tac =
+fun add_typedef_global conceal typ set opt_morphs tac =
   Named_Target.theory_init
-  #> add_typedef typ set opt_morphs tac
+  #> add_typedef conceal typ set opt_morphs tac
   #> Local_Theory.exit_result_global (apsnd o transform_info);
 
 
@@ -262,7 +263,7 @@
   let
     val args = map (apsnd (prep_constraint lthy)) raw_args;
     val ((goal, goal_pat, typedef_result), lthy') =
-      prepare_typedef prep_term (b, args, mx) set opt_morphs lthy;
+      prepare_typedef false prep_term (b, args, mx) set opt_morphs lthy;
     fun after_qed [[th]] = snd o typedef_result th;
   in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
 
diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Typedef.thy	Mon Sep 08 23:04:18 2014 +0200
@@ -108,6 +108,6 @@
 
 end
 
-ML_file "Tools/typedef.ML" setup Typedef.setup
+ML_file "Tools/typedef.ML"
 
 end