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.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;