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/function_core.ML
changeset 36936 c52d1c130898
parent 36270 fd95c0514623
child 36945 9bec62c10714 
--- a/src/HOL/Tools/Function/function_core.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sat May 15 17:59:06 2010 +0200
@@ -617,7 +617,7 @@
         local open Conv in
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
-            fconv_rule (More_Conv.binder_conv
+            fconv_rule (Conv.binder_conv
               (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
         end
isabelle