# HG changeset patch
# User blanchet
# Date 1384262674 -3600
# Node ID e95831757903d7fdc87ac84c587533649bd40309
# Parent  a2d18fea844a386bb404e30e892519c523320e5b
ported part of function package to new 'Ctr_Sugar' abstraction

diff -r a2d18fea844a -r e95831757903 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Tue Nov 12 14:00:56 2013 +0100
+++ b/src/HOL/FunDef.thy	Tue Nov 12 14:24:34 2013 +0100
@@ -310,7 +310,7 @@
 ML_file "Tools/Function/scnp_reconstruct.ML"
 ML_file "Tools/Function/fun_cases.ML"
 
-setup {* ScnpReconstruct.setup *}
+setup ScnpReconstruct.setup
 
 ML_val -- "setup inactive"
 {*
diff -r a2d18fea844a -r e95831757903 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:00:56 2013 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:24:34 2013 +0100
@@ -37,12 +37,17 @@
       let
         val (hd, args) = strip_comb t
       in
-        (((case Datatype.info_of_constr thy (dest_Const hd) of
-             SOME _ => ()
-           | NONE => err "Non-constructor pattern")
-          handle TERM ("dest_Const", _) => err "Non-constructor patterns");
-         map check_constr_pattern args;
-         ())
+        (case hd of
+          Const (hd_s, hd_T) =>
+          (case body_type hd_T of
+            Type (Tname, _) =>
+            (case Ctr_Sugar.ctr_sugar_of ctxt Tname of
+              SOME {ctrs, ...} => exists (fn Const (s, _) => s = hd_s) ctrs
+            | NONE => false)
+          | _ => false)
+        | _ => false) orelse err "Non-constructor pattern";
+        map check_constr_pattern args;
+        ()
       end
 
     val (_, qs, gs, args, _) = split_def ctxt (K true) geq
diff -r a2d18fea844a -r e95831757903 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Tue Nov 12 14:00:56 2013 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Tue Nov 12 14:24:34 2013 +0100
@@ -28,7 +28,7 @@
   val regroup_conv: string -> string -> thm list -> int list -> conv
   val regroup_union_conv: int list -> conv
 
-  val inst_constrs_of : theory -> typ -> term list
+  val inst_constrs_of: Proof.context -> typ -> term list
 end
 
 structure Function_Lib: FUNCTION_LIB =
@@ -133,10 +133,8 @@
       (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
 
 
-fun inst_constrs_of thy (T as Type (name, _)) =
-  map (fn CnCT as (_, CT) =>
-          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const CnCT))
-      (the (Datatype.get_constrs thy name))
-  | inst_constrs_of thy _ = raise Match
+fun inst_constrs_of ctxt (Type (name, Ts)) =
+    map (Ctr_Sugar.mk_ctr Ts) (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt name)))
+  | inst_constrs_of _ _ = raise Match
 
 end
diff -r a2d18fea844a -r e95831757903 src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Nov 12 14:00:56 2013 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Tue Nov 12 14:24:34 2013 +0100
@@ -6,9 +6,9 @@
 
 signature PAT_COMPLETENESS =
 sig
-    val pat_completeness_tac: Proof.context -> int -> tactic
-    val prove_completeness : Proof.context -> term list -> term -> term list list ->
-      term list list -> thm
+  val pat_completeness_tac: Proof.context -> int -> tactic
+  val prove_completeness: Proof.context -> term list -> term -> term list list ->
+    term list list -> thm
 end
 
 structure Pat_Completeness : PAT_COMPLETENESS =
@@ -94,10 +94,9 @@
   else (* Cons case *)
     let
       val thy = Proof_Context.theory_of ctxt
-      val T = fastype_of v
-      val (tname, _) = dest_Type T
-      val {exhaust=case_thm, ...} = Datatype.the_info thy tname
-      val constrs = inst_constrs_of thy T
+      val T as Type (tname, _) = fastype_of v
+      val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
+      val constrs = inst_constrs_of ctxt T
       val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
     in
       inst_case_thm thy v P case_thm
diff -r a2d18fea844a -r e95831757903 src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Tue Nov 12 14:00:56 2013 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML	Tue Nov 12 14:24:34 2013 +0100
@@ -49,7 +49,7 @@
                 map (fn (vs, subst) => (vs, (v,t)::subst)) substs
               end
           in
-            maps aux (inst_constrs_of (Proof_Context.theory_of ctxt) T)
+            maps aux (inst_constrs_of ctxt T)
           end
      | pattern_subtract_subst_aux vs t t' =
          let