# HG changeset patch
# User haftmann
# Date 1330804804 -3600
# Node ID ab4f3f765f917ce7d53930d2e77989a8f8a5b222
# Parent  44c28a33c461f8b1894a06fa0bf07e79f54c99a9
explicit locations for import_theory and setup_theory, for better user interface conformance

diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -10,7 +10,7 @@
 
 append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*};
 
-import_theory bool;
+import_theory "~~/src/HOL/Import/HOL" bool;
 
 type_maps
   bool            > HOL.bool;
@@ -39,14 +39,14 @@
 
 end_import;
 
-import_theory combin;
+import_theory "~~/src/HOL/Import/HOL" combin;
 
 const_maps
   o > Fun.comp;
 
 end_import;
 
-import_theory sum;
+import_theory "~~/src/HOL/Import/HOL" sum;
 
 type_maps
   sum > Sum_Type.sum;
@@ -70,7 +70,7 @@
 
 end_import;
 
-import_theory one;
+import_theory "~~/src/HOL/Import/HOL" one;
 
 type_maps
   one > Product_Type.unit;
@@ -86,7 +86,7 @@
 
 end_import;
 
-import_theory option;
+import_theory "~~/src/HOL/Import/HOL" option;
 
 type_maps
     option > Option.option;
@@ -111,17 +111,17 @@
 
 end_import;
 
-import_theory marker;
+import_theory "~~/src/HOL/Import/HOL" marker;
 end_import;
 
-import_theory relation;
+import_theory "~~/src/HOL/Import/HOL" relation;
 
 const_renames
   reflexive > pred_reflexive;
 
 end_import;
 
-import_theory pair;
+import_theory "~~/src/HOL/Import/HOL" pair;
 
 type_maps
     prod > Product_Type.prod;
@@ -144,7 +144,7 @@
 
 end_import;
 
-import_theory num;
+import_theory "~~/src/HOL/Import/HOL" num;
 
 type_maps
   num > Nat.nat;
@@ -164,14 +164,14 @@
 
 end_import;
 
-import_theory prim_rec;
+import_theory "~~/src/HOL/Import/HOL" prim_rec;
 
 const_maps
     "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
 
 end_import;
 
-import_theory arithmetic;
+import_theory "~~/src/HOL/Import/HOL" arithmetic;
 
 const_maps
   ALT_ZERO     > HOL4Compat.ALT_ZERO
@@ -194,29 +194,29 @@
 
 end_import;
 
-import_theory hrat;
+import_theory "~~/src/HOL/Import/HOL" hrat;
 end_import;
 
-import_theory hreal;
+import_theory "~~/src/HOL/Import/HOL" hreal;
 end_import;
 
-import_theory numeral;
+import_theory "~~/src/HOL/Import/HOL" numeral;
 end_import;
 
-import_theory ind_type;
+import_theory "~~/src/HOL/Import/HOL" ind_type;
 end_import;
 
-import_theory divides;
+import_theory "~~/src/HOL/Import/HOL" divides;
 
 const_maps
   divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
 
 end_import;
 
-import_theory prime;
+import_theory "~~/src/HOL/Import/HOL" prime;
 end_import;
 
-import_theory list;
+import_theory "~~/src/HOL/Import/HOL" list;
 
 type_maps
     list > List.list;
@@ -258,16 +258,16 @@
 
 end_import;
 
-import_theory pred_set;
+import_theory "~~/src/HOL/Import/HOL" pred_set;
 end_import;
 
-import_theory operator;
+import_theory "~~/src/HOL/Import/HOL" operator;
 end_import;
 
-import_theory rich_list;
+import_theory "~~/src/HOL/Import/HOL" rich_list;
 end_import;
 
-import_theory state_transformer;
+import_theory "~~/src/HOL/Import/HOL" state_transformer;
 end_import;
 
 append_dump "end";
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -10,32 +10,32 @@
 
 append_dump "theory HOL4Prob imports HOL4Real begin";
 
-import_theory prob_extra;
+import_theory "~~/src/HOL/Import/HOL" prob_extra;
 
 const_moves
   COMPL > GenHOL4Base.pred_set.COMPL;
 
 end_import;
 
-import_theory prob_canon;
+import_theory "~~/src/HOL/Import/HOL" prob_canon;
 end_import;
 
-import_theory boolean_sequence;
+import_theory "~~/src/HOL/Import/HOL" boolean_sequence;
 end_import;
 
-import_theory prob_algebra;
+import_theory "~~/src/HOL/Import/HOL" prob_algebra;
 end_import;
 
-import_theory prob;
+import_theory "~~/src/HOL/Import/HOL" prob;
 end_import;
 
-import_theory prob_pseudo;
+import_theory "~~/src/HOL/Import/HOL" prob_pseudo;
 end_import;
 
-import_theory prob_indep;
+import_theory "~~/src/HOL/Import/HOL" prob_indep;
 end_import;
 
-import_theory prob_uniform;
+import_theory "~~/src/HOL/Import/HOL" prob_uniform;
 end_import;
 
 append_dump "end";
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -10,7 +10,7 @@
 
 append_dump "theory HOL4Real imports HOL4Base begin";
 
-import_theory realax;
+import_theory "~~/src/HOL/Import/HOL" realax;
 
 type_maps
   real > RealDef.real;
@@ -49,7 +49,7 @@
 
 end_import;
 
-import_theory real;
+import_theory "~~/src/HOL/Import/HOL" real;
 
 const_maps
   real_gt     > HOL4Compat.real_gt
@@ -63,28 +63,28 @@
 
 end_import;
 
-import_theory topology;
+import_theory "~~/src/HOL/Import/HOL" topology;
 end_import;
 
-import_theory nets;
+import_theory "~~/src/HOL/Import/HOL" nets;
 end_import;
 
-import_theory seq;
+import_theory "~~/src/HOL/Import/HOL" seq;
 const_renames
 "-->" > "hol4-->";
 
 end_import;
 
-import_theory lim;
+import_theory "~~/src/HOL/Import/HOL" lim;
 end_import;
 
-import_theory powser;
+import_theory "~~/src/HOL/Import/HOL" powser;
 end_import;
 
-import_theory transc;
+import_theory "~~/src/HOL/Import/HOL" transc;
 end_import;
 
-import_theory poly;
+import_theory "~~/src/HOL/Import/HOL" poly;
 end_import;
 
 append_dump "end";
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -10,29 +10,29 @@
 
 append_dump "theory HOL4Vec imports HOL4Base begin";
 
-import_theory res_quan;
+import_theory "~~/src/HOL/Import/HOL" res_quan;
 end_import;
 
-import_theory word_base;
+import_theory "~~/src/HOL/Import/HOL" word_base;
 
 const_renames
   BIT > bit;
 
 end_import;
 
-import_theory word_num;
+import_theory "~~/src/HOL/Import/HOL" word_num;
 end_import;
 
-import_theory word_bitop;
+import_theory "~~/src/HOL/Import/HOL" word_bitop;
 end_import;
 
-import_theory bword_num;
+import_theory "~~/src/HOL/Import/HOL" bword_num;
 end_import;
 
-import_theory bword_arith;
+import_theory "~~/src/HOL/Import/HOL" bword_arith;
 end_import;
 
-import_theory bword_bitop;
+import_theory "~~/src/HOL/Import/HOL" bword_bitop;
 end_import;
 
 append_dump "end";
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/Generate-HOL/GenHOL4Word32.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -10,14 +10,14 @@
 
 append_dump "theory HOL4Word32 imports HOL4Base begin";
 
-import_theory bits;
+import_theory "~~/src/HOL/Import/HOL" bits;
 
 const_renames
   BIT > bit
 
 end_import;
 
-import_theory word32;
+import_theory "~~/src/HOL/Import/HOL" word32;
 
 const_renames
   "==" > EQUIV;
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -11,7 +11,7 @@
 
 ;append_dump {*theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin *}
 
-;import_theory hollight
+import_theory "~~/src/HOL/Import/HOLLight" hollight
 
 ;ignore_thms
   (* Unit type *)
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/HOL/HOL4Base.thy
--- a/src/HOL/Import/HOL/HOL4Base.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
 
 theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
 
-;setup_theory bool
+setup_theory "~~/src/HOL/Import/HOL" bool
 
 definition
   ARB :: "'a"  where
@@ -205,7 +205,7 @@
 
 ;end_setup
 
-;setup_theory combin
+setup_theory "~~/src/HOL/Import/HOL" combin
 
 definition
   K :: "'a => 'b => 'a"  where
@@ -260,7 +260,7 @@
 
 ;end_setup
 
-;setup_theory sum
+setup_theory "~~/src/HOL/Import/HOL" sum
 
 lemma ISL_OR_ISR: "ISL x | ISR x"
   sorry
@@ -279,11 +279,11 @@
 
 ;end_setup
 
-;setup_theory one
+setup_theory "~~/src/HOL/Import/HOL" one
 
 ;end_setup
 
-;setup_theory option
+setup_theory "~~/src/HOL/Import/HOL" option
 
 lemma option_CLAUSES: "(op &::bool => bool => bool)
  ((All::('a::type => bool) => bool)
@@ -477,7 +477,7 @@
 
 ;end_setup
 
-;setup_theory marker
+setup_theory "~~/src/HOL/Import/HOL" marker
 
 consts
   stmarker :: "'a => 'a" 
@@ -510,7 +510,7 @@
 
 ;end_setup
 
-;setup_theory relation
+setup_theory "~~/src/HOL/Import/HOL" relation
 
 definition
   TC :: "('a => 'a => bool) => 'a => 'a => bool"  where
@@ -758,7 +758,7 @@
 
 ;end_setup
 
-;setup_theory pair
+setup_theory "~~/src/HOL/Import/HOL" pair
 
 lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)"
   sorry
@@ -821,11 +821,11 @@
 
 ;end_setup
 
-;setup_theory num
+setup_theory "~~/src/HOL/Import/HOL" num
 
 ;end_setup
 
-;setup_theory prim_rec
+setup_theory "~~/src/HOL/Import/HOL" prim_rec
 
 lemma LESS_0_0: "0 < Suc 0"
   sorry
@@ -953,7 +953,7 @@
 
 ;end_setup
 
-;setup_theory arithmetic
+setup_theory "~~/src/HOL/Import/HOL" arithmetic
 
 definition
   nat_elim__magic :: "nat => nat"  where
@@ -1347,7 +1347,7 @@
 
 ;end_setup
 
-;setup_theory hrat
+setup_theory "~~/src/HOL/Import/HOL" hrat
 
 definition
   trat_1 :: "nat * nat"  where
@@ -1558,7 +1558,7 @@
 
 ;end_setup
 
-;setup_theory hreal
+setup_theory "~~/src/HOL/Import/HOL" hreal
 
 definition
   hrat_lt :: "hrat => hrat => bool"  where
@@ -1842,7 +1842,7 @@
 
 ;end_setup
 
-;setup_theory numeral
+setup_theory "~~/src/HOL/Import/HOL" numeral
 
 lemma numeral_suc: "Suc ALT_ZERO = NUMERAL_BIT1 ALT_ZERO &
 (ALL x. Suc (NUMERAL_BIT1 x) = NUMERAL_BIT2 x) &
@@ -2069,7 +2069,7 @@
 
 ;end_setup
 
-;setup_theory ind_type
+setup_theory "~~/src/HOL/Import/HOL" ind_type
 
 lemma INJ_INVERSE2: "(!!(x1::'A) (y1::'B) (x2::'A) y2::'B.
     ((P::'A => 'B => 'C) x1 y1 = P x2 y2) = (x1 = x2 & y1 = y2))
@@ -2304,7 +2304,7 @@
 
 ;end_setup
 
-;setup_theory divides
+setup_theory "~~/src/HOL/Import/HOL" divides
 
 lemma DIVIDES_FACT: "0 < b ==> b dvd FACT b"
   sorry
@@ -2314,7 +2314,7 @@
 
 ;end_setup
 
-;setup_theory prime
+setup_theory "~~/src/HOL/Import/HOL" prime
 
 consts
   prime :: "nat => bool" 
@@ -2333,7 +2333,7 @@
 
 ;end_setup
 
-;setup_theory list
+setup_theory "~~/src/HOL/Import/HOL" list
 
 consts
   EL :: "nat => 'a list => 'a" 
@@ -2495,7 +2495,7 @@
 
 ;end_setup
 
-;setup_theory pred_set
+setup_theory "~~/src/HOL/Import/HOL" pred_set
 
 lemma EXTENSION: "(s = t) = (ALL x. IN x s = IN x t)"
   sorry
@@ -3437,7 +3437,7 @@
 
 ;end_setup
 
-;setup_theory operator
+setup_theory "~~/src/HOL/Import/HOL" operator
 
 definition
   ASSOC :: "('a => 'a => 'a) => bool"  where
@@ -3498,7 +3498,7 @@
 
 ;end_setup
 
-;setup_theory rich_list
+setup_theory "~~/src/HOL/Import/HOL" rich_list
 
 consts
   SNOC :: "'a => 'a list => 'a list" 
@@ -4412,7 +4412,7 @@
 
 ;end_setup
 
-;setup_theory state_transformer
+setup_theory "~~/src/HOL/Import/HOL" state_transformer
 
 definition
   UNIT :: "'b => 'a => 'b * 'a"  where
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/HOL/HOL4Prob.thy
--- a/src/HOL/Import/HOL/HOL4Prob.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
 
 theory HOL4Prob imports HOL4Real begin
 
-;setup_theory prob_extra
+setup_theory "~~/src/HOL/Import/HOL" prob_extra
 
 lemma BOOL_BOOL_CASES_THM: "f = (%b. False) | f = (%b. True) | f = (%b. b) | f = Not"
   by (import prob_extra BOOL_BOOL_CASES_THM)
@@ -213,7 +213,7 @@
 
 ;end_setup
 
-;setup_theory prob_canon
+setup_theory "~~/src/HOL/Import/HOL" prob_canon
 
 consts
   alg_twin :: "bool list => bool list => bool" 
@@ -725,7 +725,7 @@
 
 ;end_setup
 
-;setup_theory boolean_sequence
+setup_theory "~~/src/HOL/Import/HOL" boolean_sequence
 
 consts
   SHD :: "(nat => bool) => bool" 
@@ -802,7 +802,7 @@
 
 ;end_setup
 
-;setup_theory prob_algebra
+setup_theory "~~/src/HOL/Import/HOL" prob_algebra
 
 consts
   alg_embed :: "bool list => (nat => bool) => bool" 
@@ -948,7 +948,7 @@
 
 ;end_setup
 
-;setup_theory prob
+setup_theory "~~/src/HOL/Import/HOL" prob
 
 consts
   alg_measure :: "bool list list => real" 
@@ -1121,7 +1121,7 @@
 
 ;end_setup
 
-;setup_theory prob_pseudo
+setup_theory "~~/src/HOL/Import/HOL" prob_pseudo
 
 consts
   pseudo_linear_hd :: "nat => bool" 
@@ -1203,7 +1203,7 @@
 
 ;end_setup
 
-;setup_theory prob_indep
+setup_theory "~~/src/HOL/Import/HOL" prob_indep
 
 consts
   indep_set :: "((nat => bool) => bool) => ((nat => bool) => bool) => bool" 
@@ -1388,7 +1388,7 @@
 
 ;end_setup
 
-;setup_theory prob_uniform
+setup_theory "~~/src/HOL/Import/HOL" prob_uniform
 
 consts
   unif_bound :: "nat => nat" 
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/HOL/HOL4Real.thy
--- a/src/HOL/Import/HOL/HOL4Real.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
 
 theory HOL4Real imports HOL4Base begin
 
-;setup_theory realax
+setup_theory "~~/src/HOL/Import/HOL" realax
 
 lemma HREAL_RDISTRIB: "hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)"
   by (import realax HREAL_RDISTRIB)
@@ -223,7 +223,7 @@
 
 ;end_setup
 
-;setup_theory real
+setup_theory "~~/src/HOL/Import/HOL" real
 
 lemma REAL_0: "(0::real) = (0::real)"
   by (import real REAL_0)
@@ -621,7 +621,7 @@
 
 ;end_setup
 
-;setup_theory topology
+setup_theory "~~/src/HOL/Import/HOL" topology
 
 definition
   re_Union :: "(('a => bool) => bool) => 'a => bool"  where
@@ -895,7 +895,7 @@
 
 ;end_setup
 
-;setup_theory nets
+setup_theory "~~/src/HOL/Import/HOL" nets
 
 definition
   dorder :: "('a => 'a => bool) => bool"  where
@@ -1057,7 +1057,7 @@
 
 ;end_setup
 
-;setup_theory seq
+setup_theory "~~/src/HOL/Import/HOL" seq
 
 consts
   "hol4-->" :: "(nat => real) => real => bool" ("hol4-->")
@@ -1338,7 +1338,7 @@
 
 ;end_setup
 
-;setup_theory lim
+setup_theory "~~/src/HOL/Import/HOL" lim
 
 definition
   tends_real_real :: "(real => real) => real => real => bool"  where
@@ -1626,7 +1626,7 @@
 
 ;end_setup
 
-;setup_theory powser
+setup_theory "~~/src/HOL/Import/HOL" powser
 
 lemma POWDIFF_LEMMA: "real.sum (0, Suc n) (%p. x ^ p * y ^ (Suc n - p)) =
 y * real.sum (0, Suc n) (%p. x ^ p * y ^ (n - p))"
@@ -1711,7 +1711,7 @@
 
 ;end_setup
 
-;setup_theory transc
+setup_theory "~~/src/HOL/Import/HOL" transc
 
 consts
   exp :: "real => real" 
@@ -2553,7 +2553,7 @@
 
 ;end_setup
 
-;setup_theory poly
+setup_theory "~~/src/HOL/Import/HOL" poly
 
 consts
   poly :: "real list => real => real" 
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/HOL/HOL4Vec.thy
--- a/src/HOL/Import/HOL/HOL4Vec.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
 
 theory HOL4Vec imports HOL4Base begin
 
-;setup_theory res_quan
+setup_theory "~~/src/HOL/Import/HOL" res_quan
 
 lemma RES_FORALL_CONJ_DIST: "RES_FORALL P (%i. Q i & R i) = (RES_FORALL P Q & RES_FORALL P R)"
   by (import res_quan RES_FORALL_CONJ_DIST)
@@ -89,7 +89,7 @@
 
 ;end_setup
 
-;setup_theory word_base
+setup_theory "~~/src/HOL/Import/HOL" word_base
 
 typedef (open) ('a) word = "{x. ALL word.
        (ALL a0. (EX a. a0 = CONSTR 0 a (%n. BOTTOM)) --> word a0) -->
@@ -403,7 +403,7 @@
 
 ;end_setup
 
-;setup_theory word_num
+setup_theory "~~/src/HOL/Import/HOL" word_num
 
 definition
   LVAL :: "('a => nat) => nat => 'a list => nat"  where
@@ -479,7 +479,7 @@
 
 ;end_setup
 
-;setup_theory word_bitop
+setup_theory "~~/src/HOL/Import/HOL" word_bitop
 
 consts
   PBITOP :: "('a word => 'b word) => bool" 
@@ -766,7 +766,7 @@
 
 ;end_setup
 
-;setup_theory bword_num
+setup_theory "~~/src/HOL/Import/HOL" bword_num
 
 definition
   BV :: "bool => nat"  where
@@ -919,7 +919,7 @@
 
 ;end_setup
 
-;setup_theory bword_arith
+setup_theory "~~/src/HOL/Import/HOL" bword_arith
 
 consts
   ACARRY :: "nat => bool word => bool word => bool => bool" 
@@ -1053,7 +1053,7 @@
 
 ;end_setup
 
-;setup_theory bword_bitop
+setup_theory "~~/src/HOL/Import/HOL" bword_bitop
 
 consts
   WNOT :: "bool word => bool word" 
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/HOL/HOL4Word32.thy
--- a/src/HOL/Import/HOL/HOL4Word32.thy	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
 
 theory HOL4Word32 imports HOL4Base begin
 
-;setup_theory bits
+setup_theory "~~/src/HOL/Import/HOL" bits
 
 consts
   DIV2 :: "nat => nat" 
@@ -285,7 +285,7 @@
 
 ;end_setup
 
-;setup_theory word32
+setup_theory "~~/src/HOL/Import/HOL" word32
 
 consts
   HB :: "nat" 
diff -r 44c28a33c461 -r ab4f3f765f91 src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/import_syntax.ML	Sat Mar 03 21:00:04 2012 +0100
@@ -30,11 +30,11 @@
 val import_segment = Parse.name >> set_import_segment
 
 
-val import_theory = Parse.name >> (fn thyname =>
+val import_theory = (Parse.name -- Parse.name) >> (fn (location, thyname) =>
                                fn thy =>
                                   thy |> set_generating_thy thyname
                                       |> Sign.add_path thyname
-                                      |> add_dump (";setup_theory " ^ thyname))
+                                      |> add_dump ("setup_theory " ^ quote location ^ " " ^ thyname))
 
 fun end_import toks =
     Scan.succeed
@@ -122,9 +122,10 @@
                                                   | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
                                       end)
 
-fun import_thy s =
+fun import_thy location s =
     let
-        val is = TextIO.openIn(s ^ ".imp")
+        val src_location = Path.append (Path.explode location) (Path.basic (s ^ ".imp"))
+        val is = TextIO.openIn (File.platform_path src_location)
         val inp = TextIO.inputAll is
         val _ = TextIO.closeIn is
         val orig_source = Source.of_string inp
@@ -148,7 +149,7 @@
         fun apply [] thy = thy
           | apply (f::fs) thy = apply fs (f thy)
     in
-        apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
+        apply (set_replaying_thy s :: Sign.add_path s :: fst (importP token_list))
     end
 
 fun create_int_thms thyname thy =
@@ -167,15 +168,15 @@
             NONE => error "Import data already cleared - forgotten a setup_theory?"
           | SOME _ => ImportData.put NONE thy
 
-val setup_theory = Parse.name
+val setup_theory = (Parse.name -- Parse.name)
                        >>
-                       (fn thyname =>
+                       (fn (location, thyname) =>
                         fn thy =>
                            (case HOL4DefThy.get thy of
                                 NoImport => thy
                               | Generating _ => error "Currently generating a theory!"
                               | Replaying _ => thy |> clear_import_thy)
-                               |> import_thy thyname
+                               |> import_thy location thyname
                                |> create_int_thms thyname)
 
 fun end_setup toks =