Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed obsolete Theory.sign_of;
authorwenzelm
Thu, 18 Aug 2005 11:17:39 +0200
changeset 17104 89d5bbb2f746
parent 17103 5a8da7720ecb
child 17105 1b07a176a880
removed obsolete Theory.sign_of;
src/Pure/Isar/args.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle