Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Statespace/state_space.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26478 9d1029ce0e13 
--- a/src/HOL/Statespace/state_space.ML	Wed Mar 19 22:50:42 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 20 00:20:44 2008 +0100
@@ -270,7 +270,7 @@
 
     fun solve_tac ctxt (_,i) st =
       let
-        val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE));
+        val distinct_thm = ProofContext.get_thm ctxt dist_thm_name;
         val goal = List.nth (cprems_of st,i-1);
         val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
       in EVERY [rtac rule i] st
isabelle