tuned;
authorwenzelm
Sun Mar 09 17:40:02 2014 +0100 (2014-03-09)
changeset 560071b61dfbcf9a4
parent 56006 6a4dcaf53664
child 56008 2897b2a4f7fd
tuned;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 09 17:37:34 2014 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 09 17:40:02 2014 +0100
     1.3 @@ -382,7 +382,7 @@
     1.4      val tsig = tsig_of ctxt;
     1.5      val class_space = Type.class_space tsig;
     1.6  
     1.7 -    val name = Type.cert_class tsig (Type.intern_class tsig xname)
     1.8 +    val name = Type.cert_class tsig (Name_Space.intern class_space xname)
     1.9        handle TYPE (msg, _, _) =>
    1.10          error (msg ^ Position.here pos ^
    1.11            Markup.markup_report (Completion.reported_text