src/HOL/Import/import_syntax.ML

+(*  Title:      HOL/Import/import_syntax.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 signature HOL4_IMPORT_SYNTAX =
 sig
     type token = OuterSyntax.token
 
     val import_segment: token list -> (theory -> theory) * token list

 	  | apply (f::fs) thy = apply fs (f thy)
     in
 	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
     end
 
+fun create_int_thms thyname thy =
+    case ImportData.get thy of
+	None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
+      | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
+
+fun clear_int_thms thy =
+    case ImportData.get thy of
+	None => error "Import data already cleared - forgotten a setup_theory?"
+      | Some _ => ImportData.put None thy
+
 val setup_theory = P.name
 		       >>
 		       (fn thyname =>
 			fn thy =>
-			   case HOL4DefThy.get thy of
-			       NoImport => thy |> import_thy thyname
-			     | Generating _ => error "Currently generating a theory!"
-			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
+			   (case HOL4DefThy.get thy of
+				NoImport => thy
+			      | Generating _ => error "Currently generating a theory!"
+			      | Replaying _ => thy |> clear_import_thy)
+			       |> import_thy thyname
+			       |> create_int_thms thyname)
 
 fun end_setup toks =
     Scan.succeed
 	(fn thy =>
 	    let
 		val thyname = get_import_thy thy
 		val segname = get_import_segment thy
 	    in
 		thy |> set_segment thyname segname
 		    |> clear_import_thy
+		    |> clear_int_thms
 		    |> Theory.parent_path
 	    end) toks
 
 val set_dump  = P.string -- P.string   >> setup_dump
 fun fl_dump toks  = Scan.succeed flush_dump toks