# HG changeset patch
# User wenzelm
# Date 1118311410 -7200
# Node ID 7c7120469f0d6b501113222e0843f457d3132f52
# Parent  b146c31a29552a7b1dfff705a4acd505a91724f6
renamed global/local_typ_raw to global/local_typ_abbrev;

diff -r b146c31a2955 -r 7c7120469f0d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Jun 09 12:03:29 2005 +0200
+++ b/src/Pure/Isar/args.ML	Thu Jun 09 12:03:30 2005 +0200
@@ -67,11 +67,11 @@
   val named_typ: (string -> typ) -> T list -> typ * T list
   val named_term: (string -> term) -> T list -> term * T list
   val named_fact: (string -> thm list) -> T list -> thm list * T list
-  val global_typ_raw: theory * T list -> typ * (theory * T list)
+  val global_typ_abbrev: theory * T list -> typ * (theory * T list)
   val global_typ: theory * T list -> typ * (theory * T list)
   val global_term: theory * T list -> term * (theory * T list)
   val global_prop: theory * T list -> term * (theory * T list)
-  val local_typ_raw: ProofContext.context * T list -> typ * (ProofContext.context * T list)
+  val local_typ_abbrev: ProofContext.context * T list -> typ * (ProofContext.context * T list)
   val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list)
   val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list)
   val local_prop: ProofContext.context * T list -> term * (ProofContext.context * T list)
@@ -292,12 +292,12 @@
 
 (* terms and types *)
 
-val global_typ_raw = Scan.peek (named_typ o ProofContext.read_typ_raw o ProofContext.init);
+val global_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o ProofContext.init);
 val global_typ = Scan.peek (named_typ o ProofContext.read_typ o ProofContext.init);
 val global_term = Scan.peek (named_term o ProofContext.read_term o ProofContext.init);
 val global_prop = Scan.peek (named_term o ProofContext.read_prop o ProofContext.init);
 
-val local_typ_raw = Scan.peek (named_typ o ProofContext.read_typ_raw);
+val local_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev);
 val local_typ = Scan.peek (named_typ o ProofContext.read_typ);
 val local_term = Scan.peek (named_term o ProofContext.read_term);
 val local_prop = Scan.peek (named_term o ProofContext.read_prop);