# HG changeset patch
# User wenzelm
# Date 1124356659 -7200
# Node ID 89d5bbb2f746d38ab57f736085389f96fcc316cb
# Parent  5a8da7720ecb3603910b4025db4917797fb0bc1b
removed obsolete Theory.sign_of;

diff -r 5a8da7720ecb -r 89d5bbb2f746 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Aug 18 11:17:38 2005 +0200
+++ b/src/Pure/Isar/args.ML	Thu Aug 18 11:17:39 2005 +0200
@@ -310,8 +310,8 @@
 val dest_tyname = fn Type (c, _) => c | TFree (a, _) => a | _ => "";
 val dest_const = fn Const (c, _) => c | Free (x, _) => x | _ => "";
 
-val global_tyname = Scan.peek (named_typ o Sign.read_tyname o Theory.sign_of) >> dest_tyname;
-val global_const = Scan.peek (named_term o Sign.read_const o Theory.sign_of) >> dest_const;
+val global_tyname = Scan.peek (named_typ o Sign.read_tyname) >> dest_tyname;
+val global_const = Scan.peek (named_term o Sign.read_const) >> dest_const;
 val local_tyname = Scan.peek (named_typ o ProofContext.read_tyname) >> dest_tyname;
 val local_const = Scan.peek (named_term o ProofContext.read_const) >> dest_const;