# HG changeset patch
# User wenzelm
# Date 1268141801 -3600
# Node ID 3007b46c1660d754cb7e73ec3258bb40cbab912e
# Parent  a91c7ed801b8178dd823b7c545408bf0b4a32fd4
ProofContext.read_class/read_type_name_proper;

diff -r a91c7ed801b8 -r 3007b46c1660 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Tue Mar 09 14:35:02 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Tue Mar 09 14:36:41 2010 +0100
@@ -102,8 +102,8 @@
 
 (* type classes *)
 
-fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
-  Sign.read_class thy s
+fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+  ProofContext.read_class ctxt s
   |> syn ? Syntax.mark_class
   |> ML_Syntax.print_string);
 
@@ -119,8 +119,8 @@
 fun type_name kind check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Type (c, _) = ProofContext.read_type_name ctxt false s;
-      val decl = Sign.the_type_decl (ProofContext.theory_of ctxt) c;
+      val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
+      val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
       val res =
         (case try check (c, decl) of
           SOME res => res