src/Pure/Isar/class.ML
changeset 25668 a9ebfc170fbc
parent 25618 01f20279fea1
child 25683 d9fefc4859be
     1.1 --- a/src/Pure/Isar/class.ML	Mon Dec 17 17:57:50 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Dec 17 17:57:51 2007 +0100
     1.3 @@ -304,7 +304,8 @@
     1.4        |> Option.map (Thm.instantiate ([],
     1.5             map (fn ((v, _), (c, ty)) => pairself (Thm.cterm_of thy)
     1.6               (Var ((v, 0), inst_ty ty), Const (c, inst_ty ty))) param_map))
     1.7 -      |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups));
     1.8 +      |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups))
     1.9 +      |> Option.map Goal.close_result;
    1.10      val axiom_premises = map_filter (#axiom o the_class_data thy) sups
    1.11        @ the_list assm_axiom;
    1.12      val axiom = case locale_intro
    1.13 @@ -321,7 +322,8 @@
    1.14      val pred_trivs = case length locale_dests
    1.15       of 0 => if is_none locale_intro then [] else [mk_pred_triv ()]
    1.16        | n => replicate n (mk_pred_triv ());
    1.17 -    val of_class = class_intro OF of_class_sups OF locale_dests OF pred_trivs;
    1.18 +    val of_class = (class_intro OF of_class_sups OF locale_dests OF pred_trivs)
    1.19 +      |> Goal.close_result;
    1.20    in (assm_intro, of_class, axiom) end;
    1.21  
    1.22  fun class_interpretation class facts defs thy =