src/Pure/pure_thy.ML
changeset 70403 468cfd56ee03
parent 70388 e31271559de8
child 71155 25b872d1d421
--- 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"