1.1 --- a/src/Pure/Isar/specification.ML	Thu Apr 29 16:53:08 2010 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Apr 29 16:55:22 2010 +0200
     1.3 @@ -284,7 +284,7 @@
     1.4  val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
     1.5  
     1.6  val notation = gen_notation (K I);
     1.7 -val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
     1.8 +val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false dummyT);
     1.9  
    1.10  end;
    1.11