1.1 --- a/src/HOL/FunDef.thy	Tue Nov 12 14:00:56 2013 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Tue Nov 12 14:24:34 2013 +0100
     1.3 @@ -310,7 +310,7 @@
     1.4  ML_file "Tools/Function/scnp_reconstruct.ML"
     1.5  ML_file "Tools/Function/fun_cases.ML"
     1.6  
     1.7 -setup {* ScnpReconstruct.setup *}
     1.8 +setup ScnpReconstruct.setup
     1.9  
    1.10  ML_val -- "setup inactive"
    1.11  {*

     2.1 --- a/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:00:56 2013 +0100
     2.2 +++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:24:34 2013 +0100
     2.3 @@ -37,12 +37,17 @@
     2.4        let
     2.5          val (hd, args) = strip_comb t
     2.6        in
     2.7 -        (((case Datatype.info_of_constr thy (dest_Const hd) of
     2.8 -             SOME _ => ()
     2.9 -           | NONE => err "Non-constructor pattern")
    2.10 -          handle TERM ("dest_Const", _) => err "Non-constructor patterns");
    2.11 -         map check_constr_pattern args;
    2.12 -         ())
    2.13 +        (case hd of
    2.14 +          Const (hd_s, hd_T) =>
    2.15 +          (case body_type hd_T of
    2.16 +            Type (Tname, _) =>
    2.17 +            (case Ctr_Sugar.ctr_sugar_of ctxt Tname of
    2.18 +              SOME {ctrs, ...} => exists (fn Const (s, _) => s = hd_s) ctrs
    2.19 +            | NONE => false)
    2.20 +          | _ => false)
    2.21 +        | _ => false) orelse err "Non-constructor pattern";
    2.22 +        map check_constr_pattern args;
    2.23 +        ()
    2.24        end
    2.25  
    2.26      val (_, qs, gs, args, _) = split_def ctxt (K true) geq

     3.1 --- a/src/HOL/Tools/Function/function_lib.ML	Tue Nov 12 14:00:56 2013 +0100
     3.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Tue Nov 12 14:24:34 2013 +0100
     3.3 @@ -28,7 +28,7 @@
     3.4    val regroup_conv: string -> string -> thm list -> int list -> conv
     3.5    val regroup_union_conv: int list -> conv
     3.6  
     3.7 -  val inst_constrs_of : theory -> typ -> term list
     3.8 +  val inst_constrs_of: Proof.context -> typ -> term list
     3.9  end
    3.10  
    3.11  structure Function_Lib: FUNCTION_LIB =
    3.12 @@ -133,10 +133,8 @@
    3.13        (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
    3.14  
    3.15  
    3.16 -fun inst_constrs_of thy (T as Type (name, _)) =
    3.17 -  map (fn CnCT as (_, CT) =>
    3.18 -          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const CnCT))
    3.19 -      (the (Datatype.get_constrs thy name))
    3.20 -  | inst_constrs_of thy _ = raise Match
    3.21 +fun inst_constrs_of ctxt (Type (name, Ts)) =
    3.22 +    map (Ctr_Sugar.mk_ctr Ts) (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt name)))
    3.23 +  | inst_constrs_of _ _ = raise Match
    3.24  
    3.25  end

     4.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Nov 12 14:00:56 2013 +0100
     4.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Tue Nov 12 14:24:34 2013 +0100
     4.3 @@ -6,9 +6,9 @@
     4.4  
     4.5  signature PAT_COMPLETENESS =
     4.6  sig
     4.7 -    val pat_completeness_tac: Proof.context -> int -> tactic
     4.8 -    val prove_completeness : Proof.context -> term list -> term -> term list list ->
     4.9 -      term list list -> thm
    4.10 +  val pat_completeness_tac: Proof.context -> int -> tactic
    4.11 +  val prove_completeness: Proof.context -> term list -> term -> term list list ->
    4.12 +    term list list -> thm
    4.13  end
    4.14  
    4.15  structure Pat_Completeness : PAT_COMPLETENESS =
    4.16 @@ -94,10 +94,9 @@
    4.17    else (* Cons case *)
    4.18      let
    4.19        val thy = Proof_Context.theory_of ctxt
    4.20 -      val T = fastype_of v
    4.21 -      val (tname, _) = dest_Type T
    4.22 -      val {exhaust=case_thm, ...} = Datatype.the_info thy tname
    4.23 -      val constrs = inst_constrs_of thy T
    4.24 +      val T as Type (tname, _) = fastype_of v
    4.25 +      val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
    4.26 +      val constrs = inst_constrs_of ctxt T
    4.27        val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
    4.28      in
    4.29        inst_case_thm thy v P case_thm

     5.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Tue Nov 12 14:00:56 2013 +0100
     5.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Tue Nov 12 14:24:34 2013 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4                  map (fn (vs, subst) => (vs, (v,t)::subst)) substs
     5.5                end
     5.6            in
     5.7 -            maps aux (inst_constrs_of (Proof_Context.theory_of ctxt) T)
     5.8 +            maps aux (inst_constrs_of ctxt T)
     5.9            end
    5.10       | pattern_subtract_subst_aux vs t t' =
    5.11           let