# HG changeset patch
# User wenzelm
# Date 1563958141 -7200
# Node ID 468cfd56ee03a1ce1230a9beb8dcb70732761d9b
# Parent  29d81b53c40bb410849bfb331fcaece4c2a5151a
avoid global syntax for MinProof (amending e31271559de8);

diff -r 29d81b53c40b -r 468cfd56ee03 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Jul 23 23:10:22 2019 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jul 24 10:49:01 2019 +0200
@@ -224,7 +224,7 @@
     (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
-    (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", Mixfix.mixfix "?")]
+    (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
   #> add_deps_const "Pure.eq"
   #> add_deps_const "Pure.imp"
   #> add_deps_const "Pure.all"