# HG changeset patch
# User haftmann
# Date 1197910671 -3600
# Node ID a9ebfc170fbc5b1c21db32ef2bc6db63df62982e
# Parent  a089038c18932e053c04614f31608d232f9980cd
closed rules

diff -r a089038c1893 -r a9ebfc170fbc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Dec 17 17:57:50 2007 +0100
+++ b/src/Pure/Isar/class.ML	Mon Dec 17 17:57:51 2007 +0100
@@ -304,7 +304,8 @@
       |> Option.map (Thm.instantiate ([],
            map (fn ((v, _), (c, ty)) => pairself (Thm.cterm_of thy)
              (Var ((v, 0), inst_ty ty), Const (c, inst_ty ty))) param_map))
-      |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups));
+      |> Option.map (MetaSimplifier.rewrite_rule (these_defs thy sups))
+      |> Option.map Goal.close_result;
     val axiom_premises = map_filter (#axiom o the_class_data thy) sups
       @ the_list assm_axiom;
     val axiom = case locale_intro
@@ -321,7 +322,8 @@
     val pred_trivs = case length locale_dests
      of 0 => if is_none locale_intro then [] else [mk_pred_triv ()]
       | n => replicate n (mk_pred_triv ());
-    val of_class = class_intro OF of_class_sups OF locale_dests OF pred_trivs;
+    val of_class = (class_intro OF of_class_sups OF locale_dests OF pred_trivs)
+      |> Goal.close_result;
   in (assm_intro, of_class, axiom) end;
 
 fun class_interpretation class facts defs thy =