# HG changeset patch # User wenzelm # Date 1192122625 -7200 # Node ID f2f4ba67cef18410e3f3b7ade875b61f55fd1e3c # Parent f2f0722675b141ecf13eaca741ba1dfb7668979c replaced Term.equiv_types by Type.similar_types; moved add_axiom/def to more_thm.ML; diff -r f2f0722675b1 -r f2f4ba67cef1 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Oct 11 19:10:24 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Thu Oct 11 19:10:25 2007 +0200 @@ -174,7 +174,7 @@ eq_heads ? (Context.mapping_result (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg') #-> (fn (lhs, _) => - Term.equiv_types (rhs, rhs') ? + Type.similar_types (rhs, rhs') ? Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)]))) end; @@ -299,19 +299,6 @@ val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term; in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end; -fun add_def (name, prop) thy = - let - val tfrees = rev (map TFree (Term.add_tfrees prop [])); - val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); - val strip_sorts = tfrees ~~ tfrees'; - val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees); - - val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; - val thy' = Theory.add_defs_i false false [(name, prop')] thy; - val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name); - val def = Thm.instantiate (recover_sorts, []) axm'; - in (Drule.unvarify def, thy') end; - in fun local_def loc kind ((c, mx), ((name, atts), rhs)) lthy1 = @@ -328,7 +315,7 @@ (*def*) val name' = Thm.def_name_optional c name; val (def, lthy3) = lthy2 - |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs'))); + |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs'))); val eq = LocalDefs.trans_terms lthy3 [(*c == loc.c xs*) lhs_def, (*lhs' == rhs'*) def, @@ -344,24 +331,11 @@ (* axioms *) -local - -fun add_axiom hyps (name, prop) thy = - let - val name' = if name = "" then "axiom_" ^ serial_string () else name; - val prop' = Logic.list_implies (hyps, prop); - val thy' = thy |> Theory.add_axioms_i [(name', prop')]; - val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name')); - val prems = map (Thm.assume o Thm.cterm_of thy') hyps; - in (Drule.implies_elim_list axm prems, thy') end; - -in - fun axioms loc kind specs lthy = let val hyps = map Thm.term_of (Assumption.assms_of lthy); fun axiom ((name, atts), props) thy = thy - |> fold_map (add_axiom hyps) (PureThy.name_multi name props) + |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props) |-> (fn ths => pair ((name, atts), [(ths, [])])); in lthy @@ -370,8 +344,6 @@ |-> local_notes loc kind end; -end; - (* init and exit *)