1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 27 14:48:46 2010 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 27 18:12:02 2010 +0100
1.3 @@ -91,10 +91,10 @@
1.4 val (c, thy') =
1.5 Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
1.6 val cdef = cname ^ "_def"
1.7 - val thy'' =
1.8 - Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
1.9 - val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
1.10 - in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
1.11 + val (ax, thy'') =
1.12 + Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
1.13 + val ax' = Drule.export_without_context ax
1.14 + in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
1.15 | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
1.16 (*Universal quant: insert a free variable into body and continue*)
1.17 let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
2.1 --- a/src/HOL/Tools/record.ML Sat Mar 27 14:48:46 2010 +0100
2.2 +++ b/src/HOL/Tools/record.ML Sat Mar 27 18:12:02 2010 +0100
2.3 @@ -272,7 +272,7 @@
2.4 infix 0 :== ===;
2.5 infixr 0 ==>;
2.6
2.7 -val op :== = Primitive_Defs.mk_defpair;
2.8 +val op :== = OldGoals.mk_defpair;
2.9 val op === = Trueprop o HOLogic.mk_eq;
2.10 val op ==> = Logic.mk_implies;
2.11
3.1 --- a/src/Pure/Proof/extraction.ML Sat Mar 27 14:48:46 2010 +0100
3.2 +++ b/src/Pure/Proof/extraction.ML Sat Mar 27 18:12:02 2010 +0100
3.3 @@ -733,7 +733,7 @@
3.4 thy'
3.5 |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
3.6 Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
3.7 - (Thm.forall_elim_var 0) (forall_intr_frees
3.8 + (Thm.forall_elim_var 0) (Thm.forall_intr_frees
3.9 (ProofChecker.thm_of_proof thy'
3.10 (fst (Proofterm.freeze_thaw_prf prf))))))
3.11 |> snd
4.1 --- a/src/Pure/Proof/proofchecker.ML Sat Mar 27 14:48:46 2010 +0100
4.2 +++ b/src/Pure/Proof/proofchecker.ML Sat Mar 27 18:12:02 2010 +0100
4.3 @@ -40,7 +40,7 @@
4.4 val ctye = map (pairself (Thm.ctyp_of thy))
4.5 (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
4.6 in
4.7 - Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
4.8 + Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
4.9 end;
4.10
4.11 fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
5.1 --- a/src/Pure/conjunction.ML Sat Mar 27 14:48:46 2010 +0100
5.2 +++ b/src/Pure/conjunction.ML Sat Mar 27 18:12:02 2010 +0100
5.3 @@ -137,7 +137,7 @@
5.4
5.5 fun comp_rule th rule =
5.6 Thm.adjust_maxidx_thm ~1 (th COMP
5.7 - (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
5.8 + (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
5.9
5.10 in
5.11
6.1 --- a/src/Pure/drule.ML Sat Mar 27 14:48:46 2010 +0100
6.2 +++ b/src/Pure/drule.ML Sat Mar 27 18:12:02 2010 +0100
6.3 @@ -16,7 +16,6 @@
6.4 val cterm_fun: (term -> term) -> (cterm -> cterm)
6.5 val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
6.6 val forall_intr_list: cterm list -> thm -> thm
6.7 - val forall_intr_frees: thm -> thm
6.8 val forall_intr_vars: thm -> thm
6.9 val forall_elim_list: cterm list -> thm -> thm
6.10 val gen_all: thm -> thm
6.11 @@ -214,16 +213,6 @@
6.12 (*Generalization over a list of variables*)
6.13 val forall_intr_list = fold_rev forall_intr;
6.14
6.15 -(*Generalization over all suitable Free variables*)
6.16 -fun forall_intr_frees th =
6.17 - let
6.18 - val thy = Thm.theory_of_thm th;
6.19 - val {prop, hyps, tpairs, ...} = rep_thm th;
6.20 - val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
6.21 - val frees = Term.fold_aterms (fn Free v =>
6.22 - if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
6.23 - in fold (forall_intr o cterm_of thy o Free) frees th end;
6.24 -
6.25 (*Generalization over Vars -- canonical order*)
6.26 fun forall_intr_vars th =
6.27 fold forall_intr
6.28 @@ -306,7 +295,7 @@
6.29
6.30 val export_without_context_open =
6.31 implies_intr_hyps
6.32 - #> forall_intr_frees
6.33 + #> Thm.forall_intr_frees
6.34 #> `Thm.maxidx_of
6.35 #-> (fn maxidx =>
6.36 Thm.forall_elim_vars (maxidx + 1)
7.1 --- a/src/Pure/more_thm.ML Sat Mar 27 14:48:46 2010 +0100
7.2 +++ b/src/Pure/more_thm.ML Sat Mar 27 18:12:02 2010 +0100
7.3 @@ -59,6 +59,7 @@
7.4 (ctyp * ctyp) list * (cterm * cterm) list
7.5 val certify_instantiate:
7.6 ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
7.7 + val forall_intr_frees: thm -> thm
7.8 val unvarify_global: thm -> thm
7.9 val close_derivation: thm -> thm
7.10 val add_axiom: binding * term -> theory -> thm * theory
7.11 @@ -295,6 +296,18 @@
7.12 Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
7.13
7.14
7.15 +(* forall_intr_frees: generalization over all suitable Free variables *)
7.16 +
7.17 +fun forall_intr_frees th =
7.18 + let
7.19 + val thy = Thm.theory_of_thm th;
7.20 + val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
7.21 + val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
7.22 + val frees = Term.fold_aterms (fn Free v =>
7.23 + if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
7.24 + in fold (Thm.forall_intr o Thm.cterm_of thy o Free) frees th end;
7.25 +
7.26 +
7.27 (* unvarify_global: global schematic variables *)
7.28
7.29 fun unvarify_global th =
7.30 @@ -334,21 +347,30 @@
7.31 fun add_axiom (b, prop) thy =
7.32 let
7.33 val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
7.34 + val _ = Sign.no_vars (Syntax.pp_global thy) prop;
7.35 val (strip, recover, prop') = stripped_sorts thy prop;
7.36 val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
7.37 val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
7.38 val thy' =
7.39 Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
7.40 val axm' = Thm.axiom thy' (Sign.full_name thy' b');
7.41 - val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
7.42 + val thm =
7.43 + Thm.instantiate (recover, []) axm'
7.44 + |> unvarify_global
7.45 + |> fold elim_implies of_sorts;
7.46 in (thm, thy') end;
7.47
7.48 fun add_def unchecked overloaded (b, prop) thy =
7.49 let
7.50 - val (strip, recover, prop') = stripped_sorts thy prop;
7.51 - val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
7.52 + val _ = Sign.no_vars (Syntax.pp_global thy) prop;
7.53 + val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
7.54 + val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
7.55 + val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
7.56 val axm' = Thm.axiom thy' (Sign.full_name thy' b);
7.57 - val thm = unvarify_global (Thm.instantiate (recover, []) axm');
7.58 + val thm =
7.59 + Thm.instantiate (recover, []) axm'
7.60 + |> unvarify_global
7.61 + |> fold_rev Thm.implies_intr prems;
7.62 in (thm, thy') end;
7.63
7.64
8.1 --- a/src/Pure/old_goals.ML Sat Mar 27 14:48:46 2010 +0100
8.2 +++ b/src/Pure/old_goals.ML Sat Mar 27 18:12:02 2010 +0100
8.3 @@ -10,6 +10,7 @@
8.4
8.5 signature OLD_GOALS =
8.6 sig
8.7 + val mk_defpair: term * term -> string * term
8.8 val strip_context: term -> (string * typ) list * term list * term
8.9 val metahyps_thms: int -> thm -> thm list option
8.10 val METAHYPS: (thm list -> tactic) -> int -> tactic
8.11 @@ -66,6 +67,13 @@
8.12 structure OldGoals: OLD_GOALS =
8.13 struct
8.14
8.15 +fun mk_defpair (lhs, rhs) =
8.16 + (case Term.head_of lhs of
8.17 + Const (name, _) =>
8.18 + (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
8.19 + | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
8.20 +
8.21 +
8.22 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
8.23 METAHYPS (fn prems => tac prems) i
8.24
9.1 --- a/src/Pure/primitive_defs.ML Sat Mar 27 14:48:46 2010 +0100
9.2 +++ b/src/Pure/primitive_defs.ML Sat Mar 27 18:12:02 2010 +0100
9.3 @@ -9,7 +9,6 @@
9.4 val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
9.5 term -> (term * term) * term
9.6 val abs_def: term -> term * term
9.7 - val mk_defpair: term * term -> string * term
9.8 end;
9.9
9.10 structure Primitive_Defs: PRIMITIVE_DEFS =
9.11 @@ -78,10 +77,4 @@
9.12 val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
9.13 in (lhs', rhs') end;
9.14
9.15 -fun mk_defpair (lhs, rhs) =
9.16 - (case Term.head_of lhs of
9.17 - Const (name, _) =>
9.18 - (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
9.19 - | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
9.20 -
9.21 end;
10.1 --- a/src/Pure/pure_thy.ML Sat Mar 27 14:48:46 2010 +0100
10.2 +++ b/src/Pure/pure_thy.ML Sat Mar 27 18:12:02 2010 +0100
10.3 @@ -200,16 +200,30 @@
10.4 (* store axioms as theorems *)
10.5
10.6 local
10.7 - fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
10.8 - let
10.9 - val thy' = add [(b, prop)] thy;
10.10 - val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
10.11 - in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
10.12 +
10.13 +fun no_read _ (_, t) = t;
10.14 +
10.15 +fun read thy (b, str) =
10.16 + Syntax.read_prop_global thy str handle ERROR msg =>
10.17 + cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
10.18 +
10.19 +fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
10.20 + let
10.21 + val prop = prep thy (b, raw_prop);
10.22 + val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
10.23 + val thm = def
10.24 + |> Thm.forall_intr_frees
10.25 + |> Thm.forall_elim_vars 0
10.26 + |> Thm.varifyT_global;
10.27 + in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
10.28 +
10.29 in
10.30 - val add_defs = add_axm o Theory.add_defs_i false;
10.31 - val add_defs_unchecked = add_axm o Theory.add_defs_i true;
10.32 - val add_defs_cmd = add_axm o Theory.add_defs false;
10.33 - val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
10.34 +
10.35 +val add_defs = add no_read false;
10.36 +val add_defs_unchecked = add no_read true;
10.37 +val add_defs_cmd = add read false;
10.38 +val add_defs_unchecked_cmd = add read true;
10.39 +
10.40 end;
10.41
10.42
11.1 --- a/src/Pure/sign.ML Sat Mar 27 14:48:46 2010 +0100
11.2 +++ b/src/Pure/sign.ML Sat Mar 27 18:12:02 2010 +0100
11.3 @@ -68,7 +68,6 @@
11.4 val cert_prop: theory -> term -> term
11.5 val no_frees: Pretty.pp -> term -> term
11.6 val no_vars: Pretty.pp -> term -> term
11.7 - val cert_def: Proof.context -> term -> (string * typ) * term
11.8 val add_defsort: string -> theory -> theory
11.9 val add_defsort_i: sort -> theory -> theory
11.10 val add_types: (binding * int * mixfix) list -> theory -> theory
11.11 @@ -332,14 +331,6 @@
11.12 val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
11.13 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
11.14
11.15 -fun cert_def ctxt tm =
11.16 - let val ((lhs, rhs), _) = tm
11.17 - |> no_vars (Syntax.pp ctxt)
11.18 - |> Logic.strip_imp_concl
11.19 - |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
11.20 - in (Term.dest_Const (Term.head_of lhs), rhs) end
11.21 - handle TERM (msg, _) => error msg;
11.22 -
11.23
11.24
11.25 (** signature extension functions **) (*exception ERROR/TYPE*)
12.1 --- a/src/Pure/term.ML Sat Mar 27 14:48:46 2010 +0100
12.2 +++ b/src/Pure/term.ML Sat Mar 27 18:12:02 2010 +0100
12.3 @@ -72,6 +72,7 @@
12.4 val map_type_tfree: (string * sort -> typ) -> typ -> typ
12.5 val map_types: (typ -> typ) -> term -> term
12.6 val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
12.7 + val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
12.8 val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
12.9 val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
12.10 val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
12.11 @@ -431,6 +432,9 @@
12.12 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
12.13 | fold_atyps f T = f T;
12.14
12.15 +fun fold_atyps_sorts f =
12.16 + fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
12.17 +
12.18 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
12.19 | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
12.20 | fold_aterms f a = f a;
13.1 --- a/src/Pure/theory.ML Sat Mar 27 14:48:46 2010 +0100
13.2 +++ b/src/Pure/theory.ML Sat Mar 27 18:12:02 2010 +0100
13.3 @@ -30,8 +30,7 @@
13.4 val end_theory: theory -> theory
13.5 val add_axiom: binding * term -> theory -> theory
13.6 val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
13.7 - val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
13.8 - val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
13.9 + val add_def: bool -> bool -> binding * term -> theory -> theory
13.10 val add_finals_i: bool -> term list -> theory -> theory
13.11 val add_finals: bool -> string list -> theory -> theory
13.12 val specify_const: (binding * typ) * mixfix -> theory -> term * theory
13.13 @@ -151,27 +150,27 @@
13.14
13.15
13.16
13.17 -(** add axioms **)
13.18 +(** primitive specifications **)
13.19
13.20 -(* prepare axioms *)
13.21 +(* raw axioms *)
13.22
13.23 fun cert_axm thy (b, raw_tm) =
13.24 let
13.25 val t = Sign.cert_prop thy raw_tm
13.26 handle TYPE (msg, _, _) => error msg
13.27 | TERM (msg, _) => error msg;
13.28 + val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
13.29 +
13.30 + val bad_sorts =
13.31 + rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
13.32 + val _ = null bad_sorts orelse
13.33 + error ("Illegal sort constraints in primitive specification: " ^
13.34 + commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
13.35 in
13.36 - Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
13.37 (b, Sign.no_vars (Syntax.pp_global thy) t)
13.38 - end;
13.39 -
13.40 -fun read_axm thy (b, str) =
13.41 - cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
13.42 + end handle ERROR msg =>
13.43 cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
13.44
13.45 -
13.46 -(* add_axiom *)
13.47 -
13.48 fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
13.49 let
13.50 val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
13.51 @@ -179,9 +178,6 @@
13.52 in axioms' end);
13.53
13.54
13.55 -
13.56 -(** add constant definitions **)
13.57 -
13.58 (* dependencies *)
13.59
13.60 fun dependencies thy unchecked def description lhs rhs =
13.61 @@ -213,7 +209,7 @@
13.62 in (t, add_deps "" const [] thy') end;
13.63
13.64
13.65 -(* check_overloading *)
13.66 +(* overloading *)
13.67
13.68 fun check_overloading thy overloaded (c, T) =
13.69 let
13.70 @@ -236,13 +232,17 @@
13.71 end;
13.72
13.73
13.74 -(* check_def *)
13.75 +(* definitional axioms *)
13.76 +
13.77 +local
13.78
13.79 fun check_def thy unchecked overloaded (b, tm) defs =
13.80 let
13.81 val ctxt = ProofContext.init thy;
13.82 val name = Sign.full_name thy b;
13.83 - val (lhs_const, rhs) = Sign.cert_def ctxt tm;
13.84 + val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
13.85 + handle TERM (msg, _) => error msg;
13.86 + val lhs_const = Term.dest_Const (Term.head_of lhs);
13.87 val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
13.88 val _ = check_overloading thy overloaded lhs_const;
13.89 in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
13.90 @@ -250,22 +250,14 @@
13.91 [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
13.92 Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
13.93
13.94 -
13.95 -(* add_defs(_i) *)
13.96 -
13.97 -local
13.98 -
13.99 -fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
13.100 - let val axms = map (prep_axm thy) raw_axms in
13.101 - thy
13.102 - |> map_defs (fold (check_def thy unchecked overloaded) axms)
13.103 - |> fold add_axiom axms
13.104 - end;
13.105 -
13.106 in
13.107
13.108 -val add_defs_i = gen_add_defs cert_axm;
13.109 -val add_defs = gen_add_defs read_axm;
13.110 +fun add_def unchecked overloaded raw_axm thy =
13.111 + let val axm = cert_axm thy raw_axm in
13.112 + thy
13.113 + |> map_defs (check_def thy unchecked overloaded axm)
13.114 + |> add_axiom axm
13.115 + end;
13.116
13.117 end;
13.118
14.1 --- a/src/Pure/thm.ML Sat Mar 27 14:48:46 2010 +0100
14.2 +++ b/src/Pure/thm.ML Sat Mar 27 18:12:02 2010 +0100
14.3 @@ -484,10 +484,7 @@
14.4 | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
14.5 let
14.6 val thy = Theory.deref thy_ref;
14.7 - val present =
14.8 - (fold_terms o fold_types o fold_atyps)
14.9 - (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
14.10 - | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
14.11 + val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
14.12 val extra = fold (Sorts.remove_sort o #2) present shyps;
14.13 val witnessed = Sign.witness_sorts thy present extra;
14.14 val extra' = fold (Sorts.remove_sort o #2) witnessed extra
15.1 --- a/src/ZF/Tools/datatype_package.ML Sat Mar 27 14:48:46 2010 +0100
15.2 +++ b/src/ZF/Tools/datatype_package.ML Sat Mar 27 18:12:02 2010 +0100
15.3 @@ -108,7 +108,7 @@
15.4 let val ncon = length con_ty_list (*number of constructors*)
15.5 fun mk_def (((id,T,syn), name, args, prems), kcon) =
15.6 (*kcon is index of constructor*)
15.7 - Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
15.8 + OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
15.9 mk_inject npart kpart
15.10 (mk_inject ncon kcon (mk_tuple args)))
15.11 in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
15.12 @@ -157,7 +157,7 @@
15.13 val case_const = Const (case_name, case_typ);
15.14 val case_tm = list_comb (case_const, case_args);
15.15
15.16 - val case_def = Primitive_Defs.mk_defpair
15.17 + val case_def = OldGoals.mk_defpair
15.18 (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
15.19
15.20
15.21 @@ -232,7 +232,7 @@
15.22 val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
15.23
15.24 val recursor_def =
15.25 - Primitive_Defs.mk_defpair
15.26 + OldGoals.mk_defpair
15.27 (recursor_tm,
15.28 @{const Univ.Vrecursor} $
15.29 absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
16.1 --- a/src/ZF/Tools/inductive_package.ML Sat Mar 27 14:48:46 2010 +0100
16.2 +++ b/src/ZF/Tools/inductive_package.ML Sat Mar 27 18:12:02 2010 +0100
16.3 @@ -156,7 +156,7 @@
16.4 val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
16.5
16.6 (*The individual sets must already be declared*)
16.7 - val axpairs = map Primitive_Defs.mk_defpair
16.8 + val axpairs = map OldGoals.mk_defpair
16.9 ((big_rec_tm, fp_rhs) ::
16.10 (case parts of
16.11 [_] => [] (*no mutual recursion*)