# HG changeset patch
# User haftmann
# Date 1232736709 -3600
# Node ID e61ba06cddcd5a89a2d198c483edbb6ef346b9b7
# Parent  1219985d24b528650dad80fb672b136da76aa606
fixed fixme

diff -r 1219985d24b5 -r e61ba06cddcd src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jan 23 19:51:49 2009 +0100
+++ b/src/Pure/Isar/class.ML	Fri Jan 23 19:51:49 2009 +0100
@@ -66,7 +66,7 @@
         val prop = thm |> Thm.prop_of |> Logic.unvarify
           |> Morphism.term (inst_morph $> eq_morph) 
           |> (map_types o map_atyps) (K aT);
-        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME*)
+        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME is WRONG!*)
           THEN ALLGOALS (ProofContext.fact_tac [thm]);
       in Goal.prove_global thy [] [] prop (tac o #context) end;
     val assm_intro = Option.map prove_assm_intro