# HG changeset patch
# User wenzelm
# Date 1124192556 -7200
# Node ID c1cd17010a1b701fc18495298107b432525abd9b
# Parent  2fae6579fb2e6eb08f8e4f4e85dff3a9c522c875
replaced sign by thy;

diff -r 2fae6579fb2e -r c1cd17010a1b src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Tue Aug 16 13:42:35 2005 +0200
+++ b/src/Pure/Isar/constdefs.ML	Tue Aug 16 13:42:36 2005 +0200
@@ -24,19 +24,18 @@
 
 (** add_constdefs(_i) **)
 
-fun pretty_const sg (c, T) =
+fun pretty_const thy (c, T) =
   Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
-    Pretty.quote (Sign.pretty_typ sg T)];
+    Pretty.quote (Sign.pretty_typ thy T)];
 
-fun pretty_constdefs sg decls =
-  Pretty.big_list "constants" (map (pretty_const sg) decls);
+fun pretty_constdefs thy decls =
+  Pretty.big_list "constants" (map (pretty_const thy) decls);
 
 fun gen_constdef prep_typ prep_term prep_att
     structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) =
   let
-    val sign = Theory.sign_of thy;
     fun err msg ts =
-      error (cat_lines (msg :: map (Sign.string_of_term sign) ts));
+      error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
 
     val ctxt =
       ProofContext.init thy |> ProofContext.add_fixes
@@ -60,7 +59,7 @@
         err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
       else ());
 
-    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;
+    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
     val name = if raw_name = "" then Thm.def_name c else raw_name;
     val atts = map (prep_att thy) raw_atts;
 
@@ -75,7 +74,7 @@
     val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs));
     val (thy', decls) = (thy, specs)
       |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);
-  in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;
+  in Pretty.writeln (pretty_constdefs thy' decls); thy' end;
 
 val add_constdefs = gen_constdefs ProofContext.read_vars_liberal
   ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute;