src/HOL/Import/import_syntax.ML
changeset 14620 1be590fd2422
parent 14518 c3019a66180f
child 14627 5d137da82f03
     1.1 --- a/src/HOL/Import/import_syntax.ML	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Import/import_syntax.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  signature HOL4_IMPORT_SYNTAX =
    1.10  sig
    1.11      type token = OuterSyntax.token
    1.12 @@ -150,14 +155,26 @@
    1.13  	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
    1.14      end
    1.15  
    1.16 +fun create_int_thms thyname thy =
    1.17 +    case ImportData.get thy of
    1.18 +	None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
    1.19 +      | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
    1.20 +
    1.21 +fun clear_int_thms thy =
    1.22 +    case ImportData.get thy of
    1.23 +	None => error "Import data already cleared - forgotten a setup_theory?"
    1.24 +      | Some _ => ImportData.put None thy
    1.25 +
    1.26  val setup_theory = P.name
    1.27  		       >>
    1.28  		       (fn thyname =>
    1.29  			fn thy =>
    1.30 -			   case HOL4DefThy.get thy of
    1.31 -			       NoImport => thy |> import_thy thyname
    1.32 -			     | Generating _ => error "Currently generating a theory!"
    1.33 -			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
    1.34 +			   (case HOL4DefThy.get thy of
    1.35 +				NoImport => thy
    1.36 +			      | Generating _ => error "Currently generating a theory!"
    1.37 +			      | Replaying _ => thy |> clear_import_thy)
    1.38 +			       |> import_thy thyname
    1.39 +			       |> create_int_thms thyname)
    1.40  
    1.41  fun end_setup toks =
    1.42      Scan.succeed
    1.43 @@ -168,6 +185,7 @@
    1.44  	    in
    1.45  		thy |> set_segment thyname segname
    1.46  		    |> clear_import_thy
    1.47 +		    |> clear_int_thms
    1.48  		    |> Theory.parent_path
    1.49  	    end) toks
    1.50