Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed fixme
authorhaftmann
Fri, 23 Jan 2009 19:51:49 +0100
changeset 29624 e61ba06cddcd
parent 29623 1219985d24b5
child 29625 a04710c3e096
fixed fixme
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle