src/HOL/Import/import_syntax.ML
changeset 14518 c3019a66180f
parent 14516 a183dec876ab
child 14620 1be590fd2422
     1.1 --- a/src/HOL/Import/import_syntax.ML	Fri Apr 02 17:40:32 2004 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Sun Apr 04 15:34:14 2004 +0200
     1.3 @@ -37,24 +37,25 @@
     1.4  				      |> Theory.add_path thyname
     1.5  				      |> add_dump (";setup_theory " ^ thyname))
     1.6  
     1.7 -val end_import = Scan.succeed
     1.8 -		     (fn thy =>
     1.9 -			 let
    1.10 -			     val thyname = get_generating_thy thy
    1.11 -			     val segname = get_import_segment thy
    1.12 -			     val (int_thms,facts) = Replay.setup_int_thms thyname thy
    1.13 -			     val thmnames = filter (not o should_ignore thyname thy) facts
    1.14 -			 in
    1.15 -			     thy |> clear_import_thy
    1.16 -				 |> set_segment thyname segname
    1.17 -				 |> set_used_names facts
    1.18 -				 |> Replay.import_thms thyname int_thms thmnames
    1.19 -				 |> clear_used_names
    1.20 -				 |> export_hol4_pending
    1.21 -				 |> Theory.parent_path
    1.22 -				 |> dump_import_thy thyname
    1.23 -				 |> add_dump ";end_setup"
    1.24 -			 end)
    1.25 +fun end_import toks =
    1.26 +    Scan.succeed
    1.27 +	(fn thy =>
    1.28 +	    let
    1.29 +		val thyname = get_generating_thy thy
    1.30 +		val segname = get_import_segment thy
    1.31 +		val (int_thms,facts) = Replay.setup_int_thms thyname thy
    1.32 +		val thmnames = filter (not o should_ignore thyname thy) facts
    1.33 +	    in
    1.34 +		thy |> clear_import_thy
    1.35 +		    |> set_segment thyname segname
    1.36 +		    |> set_used_names facts
    1.37 +		    |> Replay.import_thms thyname int_thms thmnames
    1.38 +		    |> clear_used_names
    1.39 +		    |> export_hol4_pending
    1.40 +		    |> Theory.parent_path
    1.41 +		    |> dump_import_thy thyname
    1.42 +		    |> add_dump ";end_setup"
    1.43 +	    end) toks
    1.44  
    1.45  val ignore_thms = Scan.repeat1 P.name
    1.46  			       >> (fn ignored =>
    1.47 @@ -158,18 +159,20 @@
    1.48  			     | Generating _ => error "Currently generating a theory!"
    1.49  			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
    1.50  
    1.51 -val end_setup = Scan.succeed (fn thy =>
    1.52 -				 let
    1.53 -				     val thyname = get_import_thy thy
    1.54 -				     val segname = get_import_segment thy
    1.55 -				 in
    1.56 -				     thy |> set_segment thyname segname
    1.57 -					 |> clear_import_thy
    1.58 -					 |> Theory.parent_path
    1.59 -				 end)
    1.60 +fun end_setup toks =
    1.61 +    Scan.succeed
    1.62 +	(fn thy =>
    1.63 +	    let
    1.64 +		val thyname = get_import_thy thy
    1.65 +		val segname = get_import_segment thy
    1.66 +	    in
    1.67 +		thy |> set_segment thyname segname
    1.68 +		    |> clear_import_thy
    1.69 +		    |> Theory.parent_path
    1.70 +	    end) toks
    1.71  
    1.72  val set_dump  = P.string -- P.string   >> setup_dump
    1.73 -val fl_dump   = Scan.succeed flush_dump
    1.74 +fun fl_dump toks  = Scan.succeed flush_dump toks
    1.75  val append_dump = (P.verbatim || P.string) >> add_dump
    1.76  
    1.77  val parsers =