src/Pure/more_thm.ML
changeset 35988 76ca601c941e
parent 35985 0bbf0d2348f9
child 36106 19deea200358
     1.1 --- a/src/Pure/more_thm.ML	Sat Mar 27 16:01:45 2010 +0100
     1.2 +++ b/src/Pure/more_thm.ML	Sat Mar 27 17:36:32 2010 +0100
     1.3 @@ -347,21 +347,30 @@
     1.4  fun add_axiom (b, prop) thy =
     1.5    let
     1.6      val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
     1.7 +    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     1.8      val (strip, recover, prop') = stripped_sorts thy prop;
     1.9      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
    1.10      val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
    1.11      val thy' =
    1.12        Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
    1.13      val axm' = Thm.axiom thy' (Sign.full_name thy' b');
    1.14 -    val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
    1.15 +    val thm =
    1.16 +      Thm.instantiate (recover, []) axm'
    1.17 +      |> unvarify_global
    1.18 +      |> fold elim_implies of_sorts;
    1.19    in (thm, thy') end;
    1.20  
    1.21  fun add_def unchecked overloaded (b, prop) thy =
    1.22    let
    1.23 -    val (strip, recover, prop') = stripped_sorts thy prop;
    1.24 -    val thy' = Theory.add_def unchecked overloaded (b, prop') thy;
    1.25 +    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
    1.26 +    val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
    1.27 +    val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
    1.28 +    val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
    1.29      val axm' = Thm.axiom thy' (Sign.full_name thy' b);
    1.30 -    val thm = unvarify_global (Thm.instantiate (recover, []) axm');
    1.31 +    val thm =
    1.32 +      Thm.instantiate (recover, []) axm'
    1.33 +      |> unvarify_global
    1.34 +      |> fold_rev Thm.implies_intr prems;
    1.35    in (thm, thy') end;
    1.36  
    1.37