# HG changeset patch
# User huffman
# Date 1333522810 -7200
# Node ID 9f11a3cd84b1c5c701f68a538f384925c033f8ed
# Parent  600e6b07a69361841af8ab649f08d0f7bdef43cd
rename ML structure to avoid shadowing earlier name

diff -r 600e6b07a693 -r 9f11a3cd84b1 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Wed Apr 04 07:47:42 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Wed Apr 04 09:00:10 2012 +0200
@@ -89,7 +89,7 @@
 
 text {*Initialize transfer tactic.*}
 use "transfer.ML"
-setup Transfer.setup
+setup Transfer_Principle.setup
 
 text {* Transfer introduction rules. *}
 
@@ -167,7 +167,7 @@
   "Standard = range star_of"
 
 text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* Transfer.add_const "StarDef.star_of" *}
+setup {* Transfer_Principle.add_const "StarDef.star_of" *}
 
 declare star_of_def [transfer_intro]
 
@@ -194,7 +194,7 @@
     UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
 
 text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* Transfer.add_const "StarDef.Ifun" *}
+setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
 
 lemma transfer_Ifun [transfer_intro]:
   "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -301,7 +301,7 @@
 by (simp add: unstar_def star_of_inject)
 
 text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* Transfer.add_const "StarDef.unstar" *}
+setup {* Transfer_Principle.add_const "StarDef.unstar" *}
 
 lemma transfer_unstar [transfer_intro]:
   "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
@@ -343,7 +343,7 @@
 by (simp add: Iset_def starP2_star_n)
 
 text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* Transfer.add_const "StarDef.Iset" *}
+setup {* Transfer_Principle.add_const "StarDef.Iset" *}
 
 lemma transfer_mem [transfer_intro]:
   "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
diff -r 600e6b07a693 -r 9f11a3cd84b1 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Wed Apr 04 07:47:42 2012 +0200
+++ b/src/HOL/NSA/transfer.ML	Wed Apr 04 09:00:10 2012 +0200
@@ -4,14 +4,14 @@
 Transfer principle tactic for nonstandard analysis.
 *)
 
-signature TRANSFER =
+signature TRANSFER_PRINCIPLE =
 sig
   val transfer_tac: Proof.context -> thm list -> int -> tactic
   val add_const: string -> theory -> theory
   val setup: theory -> theory
 end;
 
-structure Transfer: TRANSFER =
+structure Transfer_Principle: TRANSFER_PRINCIPLE =
 struct
 
 structure TransferData = Generic_Data