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/Function/pat_completeness.ML
changeset 42361 23f352990944
parent 37744 3daaf23b9ab4
child 47060 e2741ec9ae36 
--- a/src/HOL/Tools/Function/pat_completeness.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -128,7 +128,7 @@
 
 fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val (vs, subgf) = dest_all_all subgoal
     val (cases, _ $ thesis) = Logic.strip_horn subgf
       handle Bind => raise COMPLETENESS
isabelle