# HG changeset patch
# User wenzelm
# Date 1117729790 -7200
# Node ID 8382835019d1d7e14e3f7b977c83de20f01d4c2f
# Parent  74dc76a28038cc1b9852c811ae1a69f9cb4d7b03
Sign.restore_naming;
err_in_defn: do not apply Sign.full_name again;
tuned;

diff -r 74dc76a28038 -r 8382835019d1 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jun 02 18:29:49 2005 +0200
+++ b/src/Pure/theory.ML	Thu Jun 02 18:29:50 2005 +0200
@@ -136,7 +136,7 @@
 
 fun make_theory sign const_deps axioms oracles parents ancestors =
   Theory {sign = sign, const_deps = const_deps, axioms = axioms,
-    oracles = oracles,  parents = parents, ancestors = ancestors};
+    oracles = oracles, parents = parents, ancestors = ancestors};
 
 fun rep_theory (Theory args) = args;
 
@@ -240,7 +240,7 @@
 val no_base_names          = ext_sign (K Sign.no_base_names) ();
 val custom_accesses        = ext_sign Sign.custom_accesses;
 val set_policy             = ext_sign Sign.set_policy;
-val restore_naming         = ext_sign Sign.set_naming o Sign.naming_of o sign_of;
+val restore_naming         = ext_sign Sign.restore_naming o sign_of;
 val add_space              = ext_sign Sign.add_space;
 val hide_space             = ext_sign o Sign.hide_space;
 val hide_space_i           = ext_sign o Sign.hide_space_i;
@@ -400,8 +400,7 @@
 (* check_defn *)
 
 fun err_in_defn sg name msg =
-  (error_msg msg;
-    error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
+  error (cat_lines [msg, "The error(s) above occurred in definition " ^ quote name]);
 
 fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
 
@@ -418,10 +417,9 @@
 	end))))
   end
 
-fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
+fun check_defn sg overloaded ((deps, axms), def as (bname, tm)) =
   let
-    
-    val name = Sign.full_name sg name
+    val name = Sign.full_name sg bname;
       
     fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
       Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
@@ -510,7 +508,7 @@
 	    val _ =
 		case overloading sign c_decl ty of
 		    NoOverloading => ()
-		  | Useless => err "Sort restrictions too strong"
+		  | Useless => err "Sort constraints too strong"
 		  | Plain => (if overloaded then () else warning "Type is more general than declared")
 	    val finals = Defs.declare finals (c, c_decl) handle _ => finals
 	in
@@ -585,4 +583,3 @@
 
 structure BasicTheory: BASIC_THEORY = Theory;
 open BasicTheory;
-