replaced Term.equiv_types by Type.similar_types;
authorwenzelm
Thu Oct 11 19:10:25 2007 +0200 (2007-10-11)
changeset 24983f2f4ba67cef1
parent 24982 f2f0722675b1
child 24984 952045a8dcf2
replaced Term.equiv_types by Type.similar_types;
moved add_axiom/def to more_thm.ML;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 11 19:10:24 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 11 19:10:25 2007 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4      eq_heads ? (Context.mapping_result
     1.5        (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg')
     1.6      #-> (fn (lhs, _) =>
     1.7 -      Term.equiv_types (rhs, rhs') ?
     1.8 +      Type.similar_types (rhs, rhs') ?
     1.9          Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)])))
    1.10    end;
    1.11  
    1.12 @@ -299,19 +299,6 @@
    1.13      val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
    1.14    in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
    1.15  
    1.16 -fun add_def (name, prop) thy =
    1.17 -  let
    1.18 -    val tfrees = rev (map TFree (Term.add_tfrees prop []));
    1.19 -    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
    1.20 -    val strip_sorts = tfrees ~~ tfrees';
    1.21 -    val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
    1.22 -
    1.23 -    val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
    1.24 -    val thy' = Theory.add_defs_i false false [(name, prop')] thy;
    1.25 -    val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
    1.26 -    val def = Thm.instantiate (recover_sorts, []) axm';
    1.27 -  in (Drule.unvarify def, thy') end;
    1.28 -
    1.29  in
    1.30  
    1.31  fun local_def loc kind ((c, mx), ((name, atts), rhs)) lthy1 =
    1.32 @@ -328,7 +315,7 @@
    1.33      (*def*)
    1.34      val name' = Thm.def_name_optional c name;
    1.35      val (def, lthy3) = lthy2
    1.36 -      |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
    1.37 +      |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs')));
    1.38      val eq = LocalDefs.trans_terms lthy3
    1.39        [(*c == loc.c xs*) lhs_def,
    1.40         (*lhs' == rhs'*)  def,
    1.41 @@ -344,24 +331,11 @@
    1.42  
    1.43  (* axioms *)
    1.44  
    1.45 -local
    1.46 -
    1.47 -fun add_axiom hyps (name, prop) thy =
    1.48 -  let
    1.49 -    val name' = if name = "" then "axiom_" ^ serial_string () else name;
    1.50 -    val prop' = Logic.list_implies (hyps, prop);
    1.51 -    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
    1.52 -    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
    1.53 -    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
    1.54 -  in (Drule.implies_elim_list axm prems, thy') end;
    1.55 -
    1.56 -in
    1.57 -
    1.58  fun axioms loc kind specs lthy =
    1.59    let
    1.60      val hyps = map Thm.term_of (Assumption.assms_of lthy);
    1.61      fun axiom ((name, atts), props) thy = thy
    1.62 -      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
    1.63 +      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    1.64        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.65    in
    1.66      lthy
    1.67 @@ -370,8 +344,6 @@
    1.68      |-> local_notes loc kind
    1.69    end;
    1.70  
    1.71 -end;
    1.72 -
    1.73  
    1.74  (* init and exit *)
    1.75