# HG changeset patch
# User blanchet
# Date 1377791845 -7200
# Node ID 89f7f1cc9ae3ac1b8cadebd6b280e72d201c66f7
# Parent  cc9a2976f8363a29643e868a9f34511836acb4e0
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs

diff -r cc9a2976f836 -r 89f7f1cc9ae3 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 17:20:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 17:57:25 2013 +0200
@@ -1045,25 +1045,21 @@
     val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
+    val num_As = length unsorted_As;
     val set_bss = map (map fst o type_args_named_constrained_of) specs;
 
     val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
-      |> mk_TFrees (length unsorted_As)
+      |> mk_TFrees num_As
       ||>> mk_TFrees nn
       ||>> variant_tfrees fp_b_names;
 
-    (* TODO: Cleaner handling of fake contexts, without "background_theory". *)
+    fun add_fake_type spec =
+      Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec)
+      #>> (fn s => Type (s, unsorted_As));
 
-    fun add_fake_type spec =
-      (*The "qualify" hack below is for the case where the new type shadows an existing global type
-        defined in the same theory.*)
-      Sign.add_type no_defs_lthy (qualify false "" (type_binding_of spec),
-        length (type_args_named_constrained_of spec), mixfix_of spec);
-
-    val fake_thy = fold add_fake_type specs;
-    val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
+    val (fake_Ts, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
 
     val qsoty = quote o Syntax.string_of_typ fake_lthy;
 
@@ -1078,12 +1074,6 @@
       error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^
         "datatype specification");
 
-    fun mk_fake_T b =
-      Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
-        unsorted_As);
-
-    val fake_Ts = map mk_fake_T fp_bs;
-
     val mixfixes = map mixfix_of specs;
 
     val _ = (case duplicates Binding.eq_name fp_bs of [] => ()
@@ -1132,8 +1122,8 @@
 
     val rhsXs_As' = fold (fold (fold Term.add_tfreesT)) ctrXs_Tsss [];
     val _ = (case subtract (op =) rhsXs_As' As' of [] => ()
-      | extras => List.app (fn extra => warning ("Unused type variable: " ^ qsoty (TFree extra)))
-          extras);
+      | extras => List.app (fn extra => warning ("Unused type variable on right-hand side of " ^
+          co_prefix fp ^ "datatype definition: " ^ qsoty (TFree extra))) extras);
 
     val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
            xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
@@ -1182,13 +1172,13 @@
     val live = live_of_bnf any_fp_bnf;
     val _ =
       if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then
-        warning ("Map function and relator names ignored")
+        warning "Map function and relator names ignored"
       else
         ();
 
     val Bs =
       map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
-        (liveness_of_fp_bnf (length As) any_fp_bnf) As Bs0;
+        (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
 
     val B_ify = Term.typ_subst_atomic (As ~~ Bs);
 
@@ -1350,9 +1340,9 @@
 
               fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
                 fold_thms lthy ctr_defs'
-                   (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
-                        (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel)
-                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
+                  (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
+                       (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+                     (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
                 |> postproc
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);
 
@@ -1549,7 +1539,7 @@
    that we don't want them to be highlighted everywhere. *)
 fun extract_map_rel ("map", b) = apfst (K b)
   | extract_map_rel ("rel", b) = apsnd (K b)
-  | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);
+  | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
 
 val parse_map_rel_bindings =
   @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}