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/Quotient/quotient_tacs.ML
changeset 58950 d07464875dd4
parent 57960 ee1ba4848896
child 58956 a816aa3ff391 
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -80,7 +80,7 @@
 
 fun get_match_inst thy pat trm =
   let
-    val univ = Unify.matchers thy [(pat, trm)]
+    val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
     val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
     val tenv = Vartab.dest (Envir.term_env env)
     val tyenv = Vartab.dest (Envir.type_env env)
isabelle