# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261257711 -3600
# Node ID baac4639ecefbc9235ced2b0131e2ea5dade7c1b
# Parent  e2ac18492c68f078d1f76d4779910fab57218be8
avoided global "open"s - replaced by local "open"s

diff -r e2ac18492c68 -r baac4639ecef Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Sat Dec 19 22:21:51 2009 +0100
@@ -100,7 +100,7 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
-ML {* print_qconstinfo @{context} *}
+ML {* Quotient_Info.print_qconstinfo @{context} *}
 
 lemma plus_sym_pre:
   shows "my_plus a b \<approx> my_plus b a"
diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_def.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -13,6 +13,9 @@
 structure Quotient_Def: QUOTIENT_DEF =
 struct
 
+open Quotient_Info;
+open Quotient_Type;
+
 (* wrapper for define *)
 fun define name mx attr rhs lthy =
 let
@@ -129,6 +132,6 @@
 
 end; (* structure *)
 
-open Quotient_Def;
 
 
+
diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_info.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -262,4 +262,3 @@
 
 end; (* structure *)
 
-open Quotient_Info
diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_tacs.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -11,6 +11,11 @@
 structure Quotient_Tacs: QUOTIENT_TACS =
 struct
 
+open Quotient_Info;
+open Quotient_Type;
+open Quotient_Term;
+
+
 (* Since HOL_basic_ss is too "big" for us,    *)
 (* we need to set up our own minimal simpset. *)
 fun  mk_minimal_ss ctxt =
@@ -563,8 +568,6 @@
 in
   error msg
 end
-
-open Quotient_Term;
  
 fun procedure_inst ctxt rtrm qtrm =
 let
@@ -615,6 +618,4 @@
       (all_inj_repabs_tac ctxt, msg2),
       (clean_tac ctxt, msg3)]
 
-
-
-end;
\ No newline at end of file
+end; (* structure *)
\ No newline at end of file
diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -7,6 +7,10 @@
 structure Quotient_Term: QUOTIENT_TERM =
 struct
 
+open Quotient_Info;
+open Quotient_Type;
+open Quotient_Def;
+
 (*
 Regularizing an rtrm means:
  
diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -1,4 +1,4 @@
-signature QUOTIENT =
+signature QUOTIENT_TYPE =
 sig
   exception LIFT_MATCH of string
 
@@ -7,9 +7,11 @@
 
 end;
 
-structure Quotient: QUOTIENT =
+structure Quotient_Type: QUOTIENT_TYPE =
 struct
 
+open Quotient_Info;
+
 exception LIFT_MATCH of string
 
 (* wrappers for define, note, Attrib.internal and theorem_i *)
@@ -223,4 +225,4 @@
 
 end; (* structure *)
 
-open Quotient
+