moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
authorwenzelm
Sat Mar 27 18:07:21 2010 +0100 (2010-03-27)
changeset 359893418cdf1855e
parent 35988 76ca601c941e
child 35991 6ba552658807
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
src/HOL/Tools/record.ML
src/Pure/old_goals.ML
src/Pure/primitive_defs.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 27 17:36:32 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 27 18:07:21 2010 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4  infix 0 :== ===;
     1.5  infixr 0 ==>;
     1.6  
     1.7 -val op :== = Primitive_Defs.mk_defpair;
     1.8 +val op :== = OldGoals.mk_defpair;
     1.9  val op === = Trueprop o HOLogic.mk_eq;
    1.10  val op ==> = Logic.mk_implies;
    1.11  
     2.1 --- a/src/Pure/old_goals.ML	Sat Mar 27 17:36:32 2010 +0100
     2.2 +++ b/src/Pure/old_goals.ML	Sat Mar 27 18:07:21 2010 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4  
     2.5  signature OLD_GOALS =
     2.6  sig
     2.7 +  val mk_defpair: term * term -> string * term
     2.8    val strip_context: term -> (string * typ) list * term list * term
     2.9    val metahyps_thms: int -> thm -> thm list option
    2.10    val METAHYPS: (thm list -> tactic) -> int -> tactic
    2.11 @@ -66,6 +67,13 @@
    2.12  structure OldGoals: OLD_GOALS =
    2.13  struct
    2.14  
    2.15 +fun mk_defpair (lhs, rhs) =
    2.16 +  (case Term.head_of lhs of
    2.17 +    Const (name, _) =>
    2.18 +      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    2.19 +  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    2.20 +
    2.21 +
    2.22  (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    2.23         METAHYPS (fn prems => tac prems) i
    2.24  
     3.1 --- a/src/Pure/primitive_defs.ML	Sat Mar 27 17:36:32 2010 +0100
     3.2 +++ b/src/Pure/primitive_defs.ML	Sat Mar 27 18:07:21 2010 +0100
     3.3 @@ -9,7 +9,6 @@
     3.4    val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     3.5      term -> (term * term) * term
     3.6    val abs_def: term -> term * term
     3.7 -  val mk_defpair: term * term -> string * term
     3.8  end;
     3.9  
    3.10  structure Primitive_Defs: PRIMITIVE_DEFS =
    3.11 @@ -78,10 +77,4 @@
    3.12      val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
    3.13    in (lhs', rhs') end;
    3.14  
    3.15 -fun mk_defpair (lhs, rhs) =
    3.16 -  (case Term.head_of lhs of
    3.17 -    Const (name, _) =>
    3.18 -      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    3.19 -  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    3.20 -
    3.21  end;
     4.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Mar 27 17:36:32 2010 +0100
     4.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 27 18:07:21 2010 +0100
     4.3 @@ -108,7 +108,7 @@
     4.4      let val ncon = length con_ty_list    (*number of constructors*)
     4.5          fun mk_def (((id,T,syn), name, args, prems), kcon) =
     4.6                (*kcon is index of constructor*)
     4.7 -            Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
     4.8 +            OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
     4.9                          mk_inject npart kpart
    4.10                          (mk_inject ncon kcon (mk_tuple args)))
    4.11      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
    4.12 @@ -157,7 +157,7 @@
    4.13    val case_const = Const (case_name, case_typ);
    4.14    val case_tm = list_comb (case_const, case_args);
    4.15  
    4.16 -  val case_def = Primitive_Defs.mk_defpair
    4.17 +  val case_def = OldGoals.mk_defpair
    4.18      (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
    4.19  
    4.20  
    4.21 @@ -232,7 +232,7 @@
    4.22    val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
    4.23  
    4.24    val recursor_def =
    4.25 -      Primitive_Defs.mk_defpair
    4.26 +      OldGoals.mk_defpair
    4.27          (recursor_tm,
    4.28           @{const Univ.Vrecursor} $
    4.29             absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
     5.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Mar 27 17:36:32 2010 +0100
     5.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 27 18:07:21 2010 +0100
     5.3 @@ -156,7 +156,7 @@
     5.4    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
     5.5  
     5.6    (*The individual sets must already be declared*)
     5.7 -  val axpairs = map Primitive_Defs.mk_defpair
     5.8 +  val axpairs = map OldGoals.mk_defpair
     5.9          ((big_rec_tm, fp_rhs) ::
    5.10           (case parts of
    5.11               [_] => []                        (*no mutual recursion*)