merged
authorwenzelm
Sat Mar 27 18:12:02 2010 +0100 (2010-03-27)
changeset 359916ba552658807
parent 35990 5ceedb86aa9d
parent 35989 3418cdf1855e
child 35993 380b97496734
merged
     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 -  in
   13.29 -    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   13.30 -    (b, Sign.no_vars (Syntax.pp_global thy) t)
   13.31 -  end;
   13.32 +    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   13.33  
   13.34 -fun read_axm thy (b, str) =
   13.35 -  cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
   13.36 +    val bad_sorts =
   13.37 +      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
   13.38 +    val _ = null bad_sorts orelse
   13.39 +      error ("Illegal sort constraints in primitive specification: " ^
   13.40 +        commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
   13.41 +  in
   13.42 +    (b, Sign.no_vars (Syntax.pp_global thy) t)
   13.43 +  end handle ERROR msg =>
   13.44      cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
   13.45  
   13.46 -
   13.47 -(* add_axiom *)
   13.48 -
   13.49  fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   13.50    let
   13.51      val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
   13.52 @@ -179,9 +178,6 @@
   13.53    in axioms' end);
   13.54  
   13.55  
   13.56 -
   13.57 -(** add constant definitions **)
   13.58 -
   13.59  (* dependencies *)
   13.60  
   13.61  fun dependencies thy unchecked def description lhs rhs =
   13.62 @@ -213,7 +209,7 @@
   13.63    in (t, add_deps "" const [] thy') end;
   13.64  
   13.65  
   13.66 -(* check_overloading *)
   13.67 +(* overloading *)
   13.68  
   13.69  fun check_overloading thy overloaded (c, T) =
   13.70    let
   13.71 @@ -236,13 +232,17 @@
   13.72    end;
   13.73  
   13.74  
   13.75 -(* check_def *)
   13.76 +(* definitional axioms *)
   13.77 +
   13.78 +local
   13.79  
   13.80  fun check_def thy unchecked overloaded (b, tm) defs =
   13.81    let
   13.82      val ctxt = ProofContext.init thy;
   13.83      val name = Sign.full_name thy b;
   13.84 -    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
   13.85 +    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
   13.86 +      handle TERM (msg, _) => error msg;
   13.87 +    val lhs_const = Term.dest_Const (Term.head_of lhs);
   13.88      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   13.89      val _ = check_overloading thy overloaded lhs_const;
   13.90    in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
   13.91 @@ -250,22 +250,14 @@
   13.92     [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
   13.93      Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
   13.94  
   13.95 -
   13.96 -(* add_defs(_i) *)
   13.97 -
   13.98 -local
   13.99 -
  13.100 -fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
  13.101 -  let val axms = map (prep_axm thy) raw_axms in
  13.102 -    thy
  13.103 -    |> map_defs (fold (check_def thy unchecked overloaded) axms)
  13.104 -    |> fold add_axiom axms
  13.105 -  end;
  13.106 -
  13.107  in
  13.108  
  13.109 -val add_defs_i = gen_add_defs cert_axm;
  13.110 -val add_defs = gen_add_defs read_axm;
  13.111 +fun add_def unchecked overloaded raw_axm thy =
  13.112 +  let val axm = cert_axm thy raw_axm in
  13.113 +    thy
  13.114 +    |> map_defs (check_def thy unchecked overloaded axm)
  13.115 +    |> add_axiom axm
  13.116 +  end;
  13.117  
  13.118  end;
  13.119  
    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*)