# HG changeset patch # User wenzelm # Date 1324120237 -3600 # Node ID 0aaeb5520f2fe2853074fe5a09cc80102f282fbf # Parent 02cc5fa9c5f1d653a9bc7b146470300b57c52bd6 tuned signature; diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Dec 17 12:10:37 2011 +0100 @@ -1045,7 +1045,7 @@ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) (prems ~~ constr_defs))]); - val case_names_induct = Datatype_Data.mk_case_names_induct descr''; + val case_names_induct = Datatype.mk_case_names_induct descr''; (**** prove that new datatypes have finite support ****) diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Dec 17 12:10:37 2011 +0100 @@ -159,8 +159,8 @@ fun add_enum_type tyname tyname' thy = let - val {case_name, ...} = the (Datatype_Data.get_info thy tyname'); - val cs = map Const (the (Datatype_Data.get_constrs thy tyname')); + val {case_name, ...} = the (Datatype.get_info thy tyname'); + val cs = map Const (the (Datatype.get_constrs thy tyname')); val k = length cs; val T = Type (tyname', []); val p = Const (@{const_name pos}, T --> HOLogic.intT); @@ -195,7 +195,7 @@ (fn _ => rtac @{thm subset_antisym} 1 THEN rtac @{thm subsetI} 1 THEN - Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info + Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info (Proof_Context.theory_of lthy) tyname'))) 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of lthy))); @@ -311,7 +311,7 @@ tyname) end | SOME (T as Type (tyname, [])) => - (case Datatype_Data.get_constrs thy tyname of + (case Datatype.get_constrs thy tyname of NONE => assoc_ty_err thy T s "is not a datatype" | SOME cs => let @@ -325,7 +325,7 @@ NONE => (thy, tyname) | SOME msg => assoc_ty_err thy T s msg end)); - val cs = map Const (the (Datatype_Data.get_constrs thy' tyname)) + val cs = map Const (the (Datatype.get_constrs thy' tyname)); in ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, fold Name.declare els ctxt), @@ -825,7 +825,7 @@ handle Symtab.DUP _ => error ("SPARK type " ^ s ^ " already associated with type")) |> (fn thy' => - case Datatype_Data.get_constrs thy' tyname of + case Datatype.get_constrs thy' tyname of NONE => thy' | SOME cs => if null Ts then diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Dec 17 12:10:37 2011 +0100 @@ -623,7 +623,7 @@ |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]}, @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] -fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name) +fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name) | find_split_thm thy _ = NONE (* lifting term operations to theorems *) @@ -901,7 +901,7 @@ (*** this should be part of the datatype package ***) fun datatype_names_of_case_name thy case_name = - map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name))) + map (#1 o #2) (#descr (the (Datatype.info_of_case thy case_name))) fun make_case_distribs case_names descr thy = let diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Dec 17 12:10:37 2011 +0100 @@ -847,7 +847,7 @@ case T of TFree _ => NONE | Type (Tcon, _) => - (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of + (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of NONE => NONE | SOME cs => (case strip_comb t of diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sat Dec 17 12:10:37 2011 +0100 @@ -142,7 +142,7 @@ | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names = replace_term_and_restrict thy T t Tts free_names | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names = - case Datatype_Data.get_constrs thy Tcon of + case Datatype.get_constrs thy Tcon of NONE => replace_term_and_restrict thy T t Tts free_names | SOME constrs => (case strip_comb t of (Const (s, _), ats) => (case AList.lookup (op =) constrs s of diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/Tools/list_to_set_comprehension.ML --- a/src/HOL/Tools/list_to_set_comprehension.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/Tools/list_to_set_comprehension.ML Sat Dec 17 12:10:37 2011 +0100 @@ -93,7 +93,7 @@ in (case try dest_Const case_const of SOME (c, T) => - (case Datatype_Data.info_of_case thy c of + (case Datatype.info_of_case thy c of SOME _ => (case possible_index_of_singleton_case (fst (split_last args)) of SOME i => @@ -178,7 +178,7 @@ val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont) val x' = incr_boundvars (length vs) x val eqs' = map (incr_boundvars (length vs)) eqs - val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i + val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i val constr_t = list_comb (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))