# HG changeset patch
# User blanchet
# Date 1383666820 -3600
# Node ID 9d623cada37fa4d5b8180d1f4ec0eaa9361a1798
# Parent  113990e513fbe92d364df88a3906600d4267e2ed
avoid subtle failure in the presence of top sort

diff -r 113990e513fb -r 9d623cada37f src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:53:40 2013 +0100
@@ -199,7 +199,8 @@
                       val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
                       val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
                     in
-                      Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
+                      Term.list_comb (casex',
+                        branches' @ tap (List.app check_no_call) obj_leftovers)
                     end
                   else
                     massage_leaf bound_Ts t
@@ -345,6 +346,7 @@
     | SOME {ctrs, discs, selss, ...} =>
       let
         val thy = Proof_Context.theory_of ctxt;
+
         val gfpT = body_type (fastype_of (hd ctrs));
         val As_rho = tvar_subst thy [gfpT] [res_T];
         val substA = Term.subst_TVars As_rho;
@@ -517,10 +519,11 @@
 fun dissect_coeqn_disc seq fun_names (basic_ctr_specss : basic_corec_ctr_spec list list)
     maybe_ctr_rhs maybe_code_rhs prems' concl matchedsss =
   let
-    fun find_subterm p = let (* FIXME \<exists>? *)
-      fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v)
-        | f t = if p t then SOME t else NONE
-      in f end;
+    fun find_subterm p =
+      let (* FIXME \<exists>? *)
+        fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v)
+          | find t = if p t then SOME t else NONE;
+      in find end;
 
     val applied_fun = concl
       |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
@@ -586,7 +589,8 @@
       handle TERM _ =>
         primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
     val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name)
-      handle Option.Option => primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
+      handle Option.Option =>
+        primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
     val {ctr, ...} =
       (case maybe_of_spec of
         SOME of_spec => the (find_first (equal of_spec o #ctr) basic_ctr_specs)
@@ -850,9 +854,15 @@
 
 fun add_primcorec_ursive maybe_tac seq fixes specs maybe_of_specs lthy =
   let
+    val thy = Proof_Context.theory_of lthy;
+
     val (bs, mxs) = map_split (apfst fst) fixes;
     val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
 
+    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
+        [] => ()
+      | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
+
     val fun_names = map Binding.name_of bs;
     val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
     val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
@@ -929,7 +939,9 @@
 
         fun prove_disc ({ctr_specs, ...} : corec_spec) exclsss
             ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
-          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then [] else
+          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then
+            []
+          else
             let
               val {disc_corec, ...} = nth ctr_specs ctr_no;
               val k = 1 + ctr_no;
diff -r 113990e513fb -r 9d623cada37f src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 16:53:40 2013 +0100
@@ -464,6 +464,8 @@
 
 fun prepare_primrec fixes specs lthy =
   let
+    val thy = Proof_Context.theory_of lthy;
+
     val (bs, mxs) = map_split (apfst fst) fixes;
     val fun_names = map Binding.name_of bs;
     val eqns_data = map (dissect_eqn lthy fun_names) specs;
@@ -480,6 +482,10 @@
       |> map (partition_eq ((op =) o pairself #ctr))
       |> map (maps (map_filter (find_rec_calls has_call)));
 
+    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
+        [] => ()
+      | (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort"));
+
     val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy') =
       rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;