eliminated dead code;
authorwenzelm
Wed Sep 30 23:13:18 2009 +0200 (2009-09-30 ago)
changeset 32792a08a2b962a09
parent 32791 e6d47ce70d27
child 32793 24ba50c14ec5
eliminated dead code;
eliminated redundant parameters;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Sep 30 22:53:33 2009 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Sep 30 23:13:18 2009 +0200
     1.3 @@ -126,7 +126,6 @@
     1.4    SkipProof of int * (generic_theory * generic_theory);
     1.5      (*proof depth, resulting theory, original theory*)
     1.6  
     1.7 -val the_global_theory = fn Theory (Context.Theory thy, _) => thy | _ => raise UNDEF;
     1.8  val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
     1.9  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
    1.10  
    1.11 @@ -256,7 +255,7 @@
    1.12  
    1.13  in
    1.14  
    1.15 -fun apply_transaction pos f g (node, exit) =
    1.16 +fun apply_transaction f g (node, exit) =
    1.17    let
    1.18      val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
    1.19      val cont_node = reset_presentation node;
    1.20 @@ -293,29 +292,29 @@
    1.21  
    1.22  local
    1.23  
    1.24 -fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) =
    1.25 +fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
    1.26        State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
    1.27 -  | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
    1.28 +  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
    1.29        State (NONE, prev)
    1.30 -  | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
    1.31 +  | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
    1.32        (Runtime.controlled_execution exit thy; toplevel)
    1.33 -  | apply_tr int _ (Keep f) state =
    1.34 +  | apply_tr int (Keep f) state =
    1.35        Runtime.controlled_execution (fn x => tap (f int) x) state
    1.36 -  | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
    1.37 -      apply_transaction pos (fn x => f int x) g state
    1.38 -  | apply_tr _ _ _ _ = raise UNDEF;
    1.39 +  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
    1.40 +      apply_transaction (fn x => f int x) g state
    1.41 +  | apply_tr _ _ _ = raise UNDEF;
    1.42  
    1.43 -fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
    1.44 -  | apply_union int pos (tr :: trs) state =
    1.45 -      apply_union int pos trs state
    1.46 -        handle Runtime.UNDEF => apply_tr int pos tr state
    1.47 -          | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
    1.48 +fun apply_union _ [] state = raise FAILURE (state, UNDEF)
    1.49 +  | apply_union int (tr :: trs) state =
    1.50 +      apply_union int trs state
    1.51 +        handle Runtime.UNDEF => apply_tr int tr state
    1.52 +          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
    1.53            | exn as FAILURE _ => raise exn
    1.54            | exn => raise FAILURE (state, exn);
    1.55  
    1.56  in
    1.57  
    1.58 -fun apply_trans int pos trs state = (apply_union int pos trs state, NONE)
    1.59 +fun apply_trans int trs state = (apply_union int trs state, NONE)
    1.60    handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
    1.61  
    1.62  end;
    1.63 @@ -562,14 +561,14 @@
    1.64  
    1.65  local
    1.66  
    1.67 -fun app int (tr as Transition {trans, pos, print, no_timing, ...}) =
    1.68 +fun app int (tr as Transition {trans, print, no_timing, ...}) =
    1.69    setmp_thread_position tr (fn state =>
    1.70      let
    1.71        fun do_timing f x = (warning (command_msg "" tr); timeap f x);
    1.72        fun do_profiling f x = profile (! profiling) f x;
    1.73  
    1.74        val (result, status) =
    1.75 -         state |> (apply_trans int pos trans
    1.76 +         state |> (apply_trans int trans
    1.77            |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
    1.78            |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
    1.79