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/Ctr_Sugar/ctr_sugar_util.ML
changeset 59621 291934bac95e
parent 59617 b60e65ad13df
child 59650 ba26118128b7 
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -219,7 +219,7 @@
     val ps =
       map_filter
         (fn (_, NONE) => NONE
-          | (var, SOME ct) => SOME (Thm.cterm_of thy (Var var), ct)) (vars' ~~ cts);
+          | (var, SOME ct) => SOME (Thm.global_cterm_of thy (Var var), ct)) (vars' ~~ cts);
   in
     Drule.cterm_instantiate ps thm
   end;
isabelle