tuned signature;
authorwenzelm
Sat Dec 17 12:10:37 2011 +0100 (2011-12-17)
changeset 459060aaeb5520f2f
parent 45905 02cc5fa9c5f1
child 45907 4b41967bd77e
tuned signature;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/HOL/Tools/list_to_set_comprehension.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 16 22:07:03 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 17 12:10:37 2011 +0100
     1.3 @@ -1045,7 +1045,7 @@
     1.4              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
     1.5                  (prems ~~ constr_defs))]);
     1.6  
     1.7 -    val case_names_induct = Datatype_Data.mk_case_names_induct descr'';
     1.8 +    val case_names_induct = Datatype.mk_case_names_induct descr'';
     1.9  
    1.10      (**** prove that new datatypes have finite support ****)
    1.11  
     2.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 16 22:07:03 2011 +0100
     2.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Dec 17 12:10:37 2011 +0100
     2.3 @@ -159,8 +159,8 @@
     2.4  
     2.5  fun add_enum_type tyname tyname' thy =
     2.6    let
     2.7 -    val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
     2.8 -    val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
     2.9 +    val {case_name, ...} = the (Datatype.get_info thy tyname');
    2.10 +    val cs = map Const (the (Datatype.get_constrs thy tyname'));
    2.11      val k = length cs;
    2.12      val T = Type (tyname', []);
    2.13      val p = Const (@{const_name pos}, T --> HOLogic.intT);
    2.14 @@ -195,7 +195,7 @@
    2.15        (fn _ =>
    2.16           rtac @{thm subset_antisym} 1 THEN
    2.17           rtac @{thm subsetI} 1 THEN
    2.18 -         Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
    2.19 +         Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info
    2.20             (Proof_Context.theory_of lthy) tyname'))) 1 THEN
    2.21           ALLGOALS (asm_full_simp_tac (simpset_of lthy)));
    2.22  
    2.23 @@ -311,7 +311,7 @@
    2.24                   tyname)
    2.25                end
    2.26            | SOME (T as Type (tyname, [])) =>
    2.27 -              (case Datatype_Data.get_constrs thy tyname of
    2.28 +              (case Datatype.get_constrs thy tyname of
    2.29                   NONE => assoc_ty_err thy T s "is not a datatype"
    2.30                 | SOME cs =>
    2.31                     let
    2.32 @@ -325,7 +325,7 @@
    2.33                         NONE => (thy, tyname)
    2.34                       | SOME msg => assoc_ty_err thy T s msg
    2.35                     end));
    2.36 -        val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
    2.37 +        val cs = map Const (the (Datatype.get_constrs thy' tyname));
    2.38        in
    2.39          ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
    2.40            fold Name.declare els ctxt),
    2.41 @@ -825,7 +825,7 @@
    2.42                handle Symtab.DUP _ => error ("SPARK type " ^ s ^
    2.43                  " already associated with type")) |>
    2.44        (fn thy' =>
    2.45 -         case Datatype_Data.get_constrs thy' tyname of
    2.46 +         case Datatype.get_constrs thy' tyname of
    2.47             NONE => thy'
    2.48           | SOME cs =>
    2.49               if null Ts then
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 16 22:07:03 2011 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Dec 17 12:10:37 2011 +0100
     3.3 @@ -623,7 +623,7 @@
     3.4      |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
     3.5        @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
     3.6  
     3.7 -fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
     3.8 +fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name)
     3.9    | find_split_thm thy _ = NONE
    3.10  
    3.11  (* lifting term operations to theorems *)
    3.12 @@ -901,7 +901,7 @@
    3.13  (*** this should be part of the datatype package ***)
    3.14  
    3.15  fun datatype_names_of_case_name thy case_name =
    3.16 -  map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
    3.17 +  map (#1 o #2) (#descr (the (Datatype.info_of_case thy case_name)))
    3.18  
    3.19  fun make_case_distribs case_names descr thy =
    3.20    let
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 16 22:07:03 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Dec 17 12:10:37 2011 +0100
     4.3 @@ -847,7 +847,7 @@
     4.4      case T of
     4.5        TFree _ => NONE
     4.6      | Type (Tcon, _) =>
     4.7 -      (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of
     4.8 +      (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
     4.9          NONE => NONE
    4.10        | SOME cs =>
    4.11          (case strip_comb t of
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Fri Dec 16 22:07:03 2011 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sat Dec 17 12:10:37 2011 +0100
     5.3 @@ -142,7 +142,7 @@
     5.4        | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
     5.5          replace_term_and_restrict thy T t Tts free_names
     5.6        | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
     5.7 -        case Datatype_Data.get_constrs thy Tcon of
     5.8 +        case Datatype.get_constrs thy Tcon of
     5.9            NONE => replace_term_and_restrict thy T t Tts free_names
    5.10          | SOME constrs => (case strip_comb t of
    5.11            (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
     6.1 --- a/src/HOL/Tools/list_to_set_comprehension.ML	Fri Dec 16 22:07:03 2011 +0100
     6.2 +++ b/src/HOL/Tools/list_to_set_comprehension.ML	Sat Dec 17 12:10:37 2011 +0100
     6.3 @@ -93,7 +93,7 @@
     6.4        in
     6.5          (case try dest_Const case_const of
     6.6            SOME (c, T) =>
     6.7 -            (case Datatype_Data.info_of_case thy c of
     6.8 +            (case Datatype.info_of_case thy c of
     6.9                SOME _ =>
    6.10                  (case possible_index_of_singleton_case (fst (split_last args)) of
    6.11                    SOME i =>
    6.12 @@ -178,7 +178,7 @@
    6.13              val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
    6.14              val x' = incr_boundvars (length vs) x
    6.15              val eqs' = map (incr_boundvars (length vs)) eqs
    6.16 -            val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i
    6.17 +            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
    6.18              val constr_t =
    6.19                list_comb
    6.20                  (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))