--- a/src/Pure/Proof/proof_syntax.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Apr 12 14:38:57 2016 +0200
@@ -215,7 +215,10 @@
|> Proof_Context.init_global
|> Proof_Context.allow_dummies
|> Proof_Context.set_mode Proof_Context.mode_schematic
- |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
+ |> topsort ?
+ (Proof_Context.set_defsort [] #>
+ Config.put Type_Infer.object_logic false #>
+ Config.put Type_Infer_Context.const_sorts false);
in
fn ty => fn s =>
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s