--- a/src/HOL/Tools/Function/function.ML Fri May 09 21:03:44 2014 +0200
+++ b/src/HOL/Tools/Function/function.ML Fri May 09 22:04:50 2014 +0200
@@ -132,7 +132,9 @@
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
pelims=pelims',elims=NONE}
- val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
+ val _ =
+ Proof_Display.print_consts do_print (Position.thread_data ()) lthy
+ (K false) (map fst fixes)
in
(info,
lthy |> Local_Theory.declaration {syntax = false, pervasive = false}