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/Tools/Old_Datatype/old_datatype_aux.ML
changeset 60757 c09598a97436
parent 60328 9c94e6a30d29
child 60781 2da59cdf531c 
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -149,7 +149,7 @@
           NONE => NONE
         | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
     val indrule' = cterm_instantiate insts indrule;
-  in resolve0_tac [indrule'] i end);
+  in resolve_tac ctxt [indrule'] i end);
 
 
 (* perform exhaustive case analysis on last parameter of subgoal i *)
isabelle