src/Pure/Isar/theory_target.ML
changeset 28115 cd0d170d4dc6
parent 28094 5f340fb49b90
child 28311 b86feb50ca58
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Sep 03 17:47:38 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Sep 03 17:47:40 2008 +0200
     1.3 @@ -226,7 +226,7 @@
     1.4                  if mx3 <> NoSyn then syntax_error c'
     1.5                  else LocalTheory.theory_result (Overloading.declare (c', U))
     1.6                    ##> Overloading.confirm c
     1.7 -            | NONE => LocalTheory.theory_result (Sign.declare_const tags (c, U, mx3))));
     1.8 +            | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
     1.9      val (const, lthy') = lthy |> declare_const;
    1.10      val t = Term.list_comb (const, map Free xs);
    1.11    in
    1.12 @@ -311,33 +311,6 @@
    1.13    in ((lhs, (res_name, res)), lthy4) end;
    1.14  
    1.15  
    1.16 -(* axioms *)
    1.17 -
    1.18 -fun axioms ta kind (vars, specs) lthy =
    1.19 -  let
    1.20 -    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.21 -    val expanded_props = map (Assumption.export_term lthy thy_ctxt) (maps snd specs);
    1.22 -    val xs = fold Term.add_frees expanded_props [];
    1.23 -
    1.24 -    (*consts*)
    1.25 -    val (consts, lthy') = fold_map (declare_const ta (member (op =) xs)) vars lthy;
    1.26 -    val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    1.27 -
    1.28 -    (*axioms*)
    1.29 -    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    1.30 -    fun axiom ((name, atts), props) thy = thy
    1.31 -      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
    1.32 -      |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.33 -  in
    1.34 -    lthy'
    1.35 -    |> fold Variable.declare_term expanded_props
    1.36 -    |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)
    1.37 -    |> LocalTheory.theory_result (fold_map axiom specs)
    1.38 -    |-> notes ta kind
    1.39 -    |>> pair (map #1 consts)
    1.40 -  end;
    1.41 -
    1.42 -
    1.43  (* init *)
    1.44  
    1.45  local
    1.46 @@ -357,7 +330,6 @@
    1.47    Data.put ta #>
    1.48    LocalTheory.init (NameSpace.base target)
    1.49     {pretty = pretty ta,
    1.50 -    axioms = axioms ta,
    1.51      abbrev = abbrev ta,
    1.52      define = define ta,
    1.53      notes = notes ta,