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/Prolog/prolog.ML
changeset 36945 9bec62c10714
parent 35232 f588e1169c8b
child 38549 d0385f2764d8 
--- a/src/HOL/Prolog/prolog.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Sat May 15 21:50:05 2010 +0200
@@ -82,7 +82,7 @@
         val (prems, Const("Trueprop", _)$concl) = rep_goal
                                                 (#3(dest_state (st,i)));
 *)
-        val subgoal = #3(dest_state (st,i));
+        val subgoal = #3(Thm.dest_state (st,i));
         val prems = Logic.strip_assums_hyp subgoal;
         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
         fun drot_tac k i = DETERM (rotate_tac k i);
isabelle