# HG changeset patch
# User wenzelm
# Date 1269709641 -3600
# Node ID 3418cdf1855e2fc32b63c2b76f4a001549cb01ec
# Parent  76ca601c941e7b50c17903811fe165a197e18075
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;

diff -r 76ca601c941e -r 3418cdf1855e src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Mar 27 17:36:32 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 27 18:07:21 2010 +0100
@@ -272,7 +272,7 @@
 infix 0 :== ===;
 infixr 0 ==>;
 
-val op :== = Primitive_Defs.mk_defpair;
+val op :== = OldGoals.mk_defpair;
 val op === = Trueprop o HOLogic.mk_eq;
 val op ==> = Logic.mk_implies;
 
diff -r 76ca601c941e -r 3418cdf1855e src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Sat Mar 27 17:36:32 2010 +0100
+++ b/src/Pure/old_goals.ML	Sat Mar 27 18:07:21 2010 +0100
@@ -10,6 +10,7 @@
 
 signature OLD_GOALS =
 sig
+  val mk_defpair: term * term -> string * term
   val strip_context: term -> (string * typ) list * term list * term
   val metahyps_thms: int -> thm -> thm list option
   val METAHYPS: (thm list -> tactic) -> int -> tactic
@@ -66,6 +67,13 @@
 structure OldGoals: OLD_GOALS =
 struct
 
+fun mk_defpair (lhs, rhs) =
+  (case Term.head_of lhs of
+    Const (name, _) =>
+      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
+  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
+
+
 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
        METAHYPS (fn prems => tac prems) i
 
diff -r 76ca601c941e -r 3418cdf1855e src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Mar 27 17:36:32 2010 +0100
+++ b/src/Pure/primitive_defs.ML	Sat Mar 27 18:07:21 2010 +0100
@@ -9,7 +9,6 @@
   val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     term -> (term * term) * term
   val abs_def: term -> term * term
-  val mk_defpair: term * term -> string * term
 end;
 
 structure Primitive_Defs: PRIMITIVE_DEFS =
@@ -78,10 +77,4 @@
     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   in (lhs', rhs') end;
 
-fun mk_defpair (lhs, rhs) =
-  (case Term.head_of lhs of
-    Const (name, _) =>
-      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
-  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
-
 end;
diff -r 76ca601c941e -r 3418cdf1855e src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Mar 27 17:36:32 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 27 18:07:21 2010 +0100
@@ -108,7 +108,7 @@
     let val ncon = length con_ty_list    (*number of constructors*)
         fun mk_def (((id,T,syn), name, args, prems), kcon) =
               (*kcon is index of constructor*)
-            Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
+            OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
                         mk_inject npart kpart
                         (mk_inject ncon kcon (mk_tuple args)))
     in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
@@ -157,7 +157,7 @@
   val case_const = Const (case_name, case_typ);
   val case_tm = list_comb (case_const, case_args);
 
-  val case_def = Primitive_Defs.mk_defpair
+  val case_def = OldGoals.mk_defpair
     (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
@@ -232,7 +232,7 @@
   val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
 
   val recursor_def =
-      Primitive_Defs.mk_defpair
+      OldGoals.mk_defpair
         (recursor_tm,
          @{const Univ.Vrecursor} $
            absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
diff -r 76ca601c941e -r 3418cdf1855e src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Mar 27 17:36:32 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 27 18:07:21 2010 +0100
@@ -156,7 +156,7 @@
   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
   (*The individual sets must already be declared*)
-  val axpairs = map Primitive_Defs.mk_defpair
+  val axpairs = map OldGoals.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)