1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:53:40 2013 +0100
     1.3 @@ -199,7 +199,8 @@
     1.4                        val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
     1.5                        val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
     1.6                      in
     1.7 -                      Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
     1.8 +                      Term.list_comb (casex',
     1.9 +                        branches' @ tap (List.app check_no_call) obj_leftovers)
    1.10                      end
    1.11                    else
    1.12                      massage_leaf bound_Ts t
    1.13 @@ -345,6 +346,7 @@
    1.14      | SOME {ctrs, discs, selss, ...} =>
    1.15        let
    1.16          val thy = Proof_Context.theory_of ctxt;
    1.17 +
    1.18          val gfpT = body_type (fastype_of (hd ctrs));
    1.19          val As_rho = tvar_subst thy [gfpT] [res_T];
    1.20          val substA = Term.subst_TVars As_rho;
    1.21 @@ -517,10 +519,11 @@
    1.22  fun dissect_coeqn_disc seq fun_names (basic_ctr_specss : basic_corec_ctr_spec list list)
    1.23      maybe_ctr_rhs maybe_code_rhs prems' concl matchedsss =
    1.24    let
    1.25 -    fun find_subterm p = let (* FIXME \<exists>? *)
    1.26 -      fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v)
    1.27 -        | f t = if p t then SOME t else NONE
    1.28 -      in f end;
    1.29 +    fun find_subterm p =
    1.30 +      let (* FIXME \<exists>? *)
    1.31 +        fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v)
    1.32 +          | find t = if p t then SOME t else NONE;
    1.33 +      in find end;
    1.34  
    1.35      val applied_fun = concl
    1.36        |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
    1.37 @@ -586,7 +589,8 @@
    1.38        handle TERM _ =>
    1.39          primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
    1.40      val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name)
    1.41 -      handle Option.Option => primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
    1.42 +      handle Option.Option =>
    1.43 +        primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
    1.44      val {ctr, ...} =
    1.45        (case maybe_of_spec of
    1.46          SOME of_spec => the (find_first (equal of_spec o #ctr) basic_ctr_specs)
    1.47 @@ -850,9 +854,15 @@
    1.48  
    1.49  fun add_primcorec_ursive maybe_tac seq fixes specs maybe_of_specs lthy =
    1.50    let
    1.51 +    val thy = Proof_Context.theory_of lthy;
    1.52 +
    1.53      val (bs, mxs) = map_split (apfst fst) fixes;
    1.54      val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
    1.55  
    1.56 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
    1.57 +        [] => ()
    1.58 +      | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
    1.59 +
    1.60      val fun_names = map Binding.name_of bs;
    1.61      val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
    1.62      val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
    1.63 @@ -929,7 +939,9 @@
    1.64  
    1.65          fun prove_disc ({ctr_specs, ...} : corec_spec) exclsss
    1.66              ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
    1.67 -          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then [] else
    1.68 +          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then
    1.69 +            []
    1.70 +          else
    1.71              let
    1.72                val {disc_corec, ...} = nth ctr_specs ctr_no;
    1.73                val k = 1 + ctr_no;

     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 16:53:40 2013 +0100
     2.3 @@ -464,6 +464,8 @@
     2.4  
     2.5  fun prepare_primrec fixes specs lthy =
     2.6    let
     2.7 +    val thy = Proof_Context.theory_of lthy;
     2.8 +
     2.9      val (bs, mxs) = map_split (apfst fst) fixes;
    2.10      val fun_names = map Binding.name_of bs;
    2.11      val eqns_data = map (dissect_eqn lthy fun_names) specs;
    2.12 @@ -480,6 +482,10 @@
    2.13        |> map (partition_eq ((op =) o pairself #ctr))
    2.14        |> map (maps (map_filter (find_rec_calls has_call)));
    2.15  
    2.16 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
    2.17 +        [] => ()
    2.18 +      | (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort"));
    2.19 +
    2.20      val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy') =
    2.21        rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
    2.22