Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_tacs.ML
changeset 871 4163fe3dbf8c
parent 870 2a19e0a37131
child 896 4e0b89d886ac 
--- a/Quot/quotient_tacs.ML	Thu Jan 14 10:47:19 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 14 10:51:03 2010 +0100
@@ -503,9 +503,7 @@
 *)
 fun clean_tac lthy =
 let
-  (* FIXME/TODO produce defs with lthy, like prs and ids *)
-  val thy = ProofContext.theory_of lthy;
-  val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+  val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy)
   (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
   val prs = prs_rules_get lthy
   val ids = id_simps_get lthy
nominal2