# HG changeset patch
# User wenzelm
# Date 1269709922 -3600
# Node ID 6ba5526588072325330c859cc5ca0c33c93e5759
# Parent  5ceedb86aa9d7462391aebc229abef57ec7be74c# Parent  3418cdf1855e2fc32b63c2b76f4a001549cb01ec
merged

diff -r 5ceedb86aa9d -r 6ba552658807 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -91,10 +91,10 @@
             val (c, thy') =
               Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
             val cdef = cname ^ "_def"
-            val thy'' =
-              Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
-            val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
-          in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
+            val (ax, thy'') =
+              Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
+            val ax' = Drule.export_without_context ax
+          in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
       | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
           (*Universal quant: insert a free variable into body and continue*)
           let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
diff -r 5ceedb86aa9d -r 6ba552658807 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 27 18:12:02 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 5ceedb86aa9d -r 6ba552658807 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -733,7 +733,7 @@
              thy'
              |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
                   Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
-                    (Thm.forall_elim_var 0) (forall_intr_frees
+                    (Thm.forall_elim_var 0) (Thm.forall_intr_frees
                       (ProofChecker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -40,7 +40,7 @@
         val ctye = map (pairself (Thm.ctyp_of thy))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
       in
-        Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
+        Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
       end;
 
     fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/conjunction.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -137,7 +137,7 @@
 
 fun comp_rule th rule =
   Thm.adjust_maxidx_thm ~1 (th COMP
-    (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
+    (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
 
 in
 
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/drule.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -16,7 +16,6 @@
   val cterm_fun: (term -> term) -> (cterm -> cterm)
   val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
   val forall_intr_list: cterm list -> thm -> thm
-  val forall_intr_frees: thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
   val gen_all: thm -> thm
@@ -214,16 +213,6 @@
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev forall_intr;
 
-(*Generalization over all suitable Free variables*)
-fun forall_intr_frees th =
-    let
-      val thy = Thm.theory_of_thm th;
-      val {prop, hyps, tpairs, ...} = rep_thm th;
-      val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
-      val frees = Term.fold_aterms (fn Free v =>
-        if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
-    in fold (forall_intr o cterm_of thy o Free) frees th end;
-
 (*Generalization over Vars -- canonical order*)
 fun forall_intr_vars th =
   fold forall_intr
@@ -306,7 +295,7 @@
 
 val export_without_context_open =
   implies_intr_hyps
-  #> forall_intr_frees
+  #> Thm.forall_intr_frees
   #> `Thm.maxidx_of
   #-> (fn maxidx =>
     Thm.forall_elim_vars (maxidx + 1)
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -59,6 +59,7 @@
     (ctyp * ctyp) list * (cterm * cterm) list
   val certify_instantiate:
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+  val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
   val close_derivation: thm -> thm
   val add_axiom: binding * term -> theory -> thm * theory
@@ -295,6 +296,18 @@
   Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
 
 
+(* forall_intr_frees: generalization over all suitable Free variables *)
+
+fun forall_intr_frees th =
+  let
+    val thy = Thm.theory_of_thm th;
+    val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
+    val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
+    val frees = Term.fold_aterms (fn Free v =>
+      if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
+  in fold (Thm.forall_intr o Thm.cterm_of thy o Free) frees th end;
+
+
 (* unvarify_global: global schematic variables *)
 
 fun unvarify_global th =
@@ -334,21 +347,30 @@
 fun add_axiom (b, prop) thy =
   let
     val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
     val thy' =
       Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b');
-    val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
+    val thm =
+      Thm.instantiate (recover, []) axm'
+      |> unvarify_global
+      |> fold elim_implies of_sorts;
   in (thm, thy') end;
 
 fun add_def unchecked overloaded (b, prop) thy =
   let
-    val (strip, recover, prop') = stripped_sorts thy prop;
-    val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
+    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+    val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
+    val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
+    val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b);
-    val thm = unvarify_global (Thm.instantiate (recover, []) axm');
+    val thm =
+      Thm.instantiate (recover, []) axm'
+      |> unvarify_global
+      |> fold_rev Thm.implies_intr prems;
   in (thm, thy') end;
 
 
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/old_goals.ML	Sat Mar 27 18:12:02 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 5ceedb86aa9d -r 6ba552658807 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/primitive_defs.ML	Sat Mar 27 18:12:02 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 5ceedb86aa9d -r 6ba552658807 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/pure_thy.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -200,16 +200,30 @@
 (* store axioms as theorems *)
 
 local
-  fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
-    let
-      val thy' = add [(b, prop)] thy;
-      val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
-    in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
+
+fun no_read _ (_, t) = t;
+
+fun read thy (b, str) =
+  Syntax.read_prop_global thy str handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
+
+fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
+  let
+    val prop = prep thy (b, raw_prop);
+    val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+    val thm = def
+      |> Thm.forall_intr_frees
+      |> Thm.forall_elim_vars 0
+      |> Thm.varifyT_global;
+  in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
+
 in
-  val add_defs               = add_axm o Theory.add_defs_i false;
-  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
-  val add_defs_cmd           = add_axm o Theory.add_defs false;
-  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
+
+val add_defs = add no_read false;
+val add_defs_unchecked = add no_read true;
+val add_defs_cmd = add read false;
+val add_defs_unchecked_cmd = add read true;
+
 end;
 
 
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/sign.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -68,7 +68,6 @@
   val cert_prop: theory -> term -> term
   val no_frees: Pretty.pp -> term -> term
   val no_vars: Pretty.pp -> term -> term
-  val cert_def: Proof.context -> term -> (string * typ) * term
   val add_defsort: string -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (binding * int * mixfix) list -> theory -> theory
@@ -332,14 +331,6 @@
 val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
 
-fun cert_def ctxt tm =
-  let val ((lhs, rhs), _) = tm
-    |> no_vars (Syntax.pp ctxt)
-    |> Logic.strip_imp_concl
-    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
-  in (Term.dest_Const (Term.head_of lhs), rhs) end
-  handle TERM (msg, _) => error msg;
-
 
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/term.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -72,6 +72,7 @@
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
   val map_types: (typ -> typ) -> term -> term
   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
+  val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
@@ -431,6 +432,9 @@
 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   | fold_atyps f T = f T;
 
+fun fold_atyps_sorts f =
+  fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
+
 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   | fold_aterms f a = f a;
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/theory.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -30,8 +30,7 @@
   val end_theory: theory -> theory
   val add_axiom: binding * term -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
-  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
-  val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
+  val add_def: bool -> bool -> binding * term -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
@@ -151,27 +150,27 @@
 
 
 
-(** add axioms **)
+(** primitive specifications **)
 
-(* prepare axioms *)
+(* raw axioms *)
 
 fun cert_axm thy (b, raw_tm) =
   let
     val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
-  in
-    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
-    (b, Sign.no_vars (Syntax.pp_global thy) t)
-  end;
+    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
 
-fun read_axm thy (b, str) =
-  cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
+    val bad_sorts =
+      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
+    val _ = null bad_sorts orelse
+      error ("Illegal sort constraints in primitive specification: " ^
+        commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
+  in
+    (b, Sign.no_vars (Syntax.pp_global thy) t)
+  end handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
-
-(* add_axiom *)
-
 fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   let
     val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
@@ -179,9 +178,6 @@
   in axioms' end);
 
 
-
-(** add constant definitions **)
-
 (* dependencies *)
 
 fun dependencies thy unchecked def description lhs rhs =
@@ -213,7 +209,7 @@
   in (t, add_deps "" const [] thy') end;
 
 
-(* check_overloading *)
+(* overloading *)
 
 fun check_overloading thy overloaded (c, T) =
   let
@@ -236,13 +232,17 @@
   end;
 
 
-(* check_def *)
+(* definitional axioms *)
+
+local
 
 fun check_def thy unchecked overloaded (b, tm) defs =
   let
     val ctxt = ProofContext.init thy;
     val name = Sign.full_name thy b;
-    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
+    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
+      handle TERM (msg, _) => error msg;
+    val lhs_const = Term.dest_Const (Term.head_of lhs);
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
@@ -250,22 +250,14 @@
    [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
 
-
-(* add_defs(_i) *)
-
-local
-
-fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
-  let val axms = map (prep_axm thy) raw_axms in
-    thy
-    |> map_defs (fold (check_def thy unchecked overloaded) axms)
-    |> fold add_axiom axms
-  end;
-
 in
 
-val add_defs_i = gen_add_defs cert_axm;
-val add_defs = gen_add_defs read_axm;
+fun add_def unchecked overloaded raw_axm thy =
+  let val axm = cert_axm thy raw_axm in
+    thy
+    |> map_defs (check_def thy unchecked overloaded axm)
+    |> add_axiom axm
+  end;
 
 end;
 
diff -r 5ceedb86aa9d -r 6ba552658807 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/thm.ML	Sat Mar 27 18:12:02 2010 +0100
@@ -484,10 +484,7 @@
   | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
       let
         val thy = Theory.deref thy_ref;
-        val present =
-          (fold_terms o fold_types o fold_atyps)
-            (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
-              | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
+        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
         val extra' = fold (Sorts.remove_sort o #2) witnessed extra
diff -r 5ceedb86aa9d -r 6ba552658807 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 27 18:12:02 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 5ceedb86aa9d -r 6ba552658807 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Mar 27 14:48:46 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 27 18:12:02 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*)