src/Pure/Isar/toplevel.ML
changeset 33390 5b499f36dd25
parent 33223 d27956b4d3b4
child 33519 e31a85f92ce9
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Nov 02 20:57:48 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Nov 02 21:03:41 2009 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
     1.5    val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
     1.6    val proof: (Proof.state -> Proof.state) -> transition -> transition
     1.7 -  val actual_proof: (ProofNode.T -> ProofNode.T) -> transition -> transition
     1.8 +  val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
     1.9    val skip_proof: (int -> int) -> transition -> transition
    1.10    val skip_proof_to_theory: (int -> bool) -> transition -> transition
    1.11    val get_id: transition -> string option
    1.12 @@ -121,7 +121,7 @@
    1.13  datatype node =
    1.14    Theory of generic_theory * Proof.context option
    1.15      (*theory with presentation context*) |
    1.16 -  Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory)
    1.17 +  Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
    1.18      (*proof node, finish, original theory*) |
    1.19    SkipProof of int * (generic_theory * generic_theory);
    1.20      (*proof depth, resulting theory, original theory*)
    1.21 @@ -130,7 +130,7 @@
    1.22  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
    1.23  
    1.24  fun cases_node f _ (Theory (gthy, _)) = f gthy
    1.25 -  | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf)
    1.26 +  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
    1.27    | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
    1.28  
    1.29  val context_node = cases_node Context.proof_of Proof.context_of;
    1.30 @@ -148,7 +148,7 @@
    1.31  
    1.32  fun level (State (NONE, _)) = 0
    1.33    | level (State (SOME (Theory _, _), _)) = 0
    1.34 -  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf)
    1.35 +  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
    1.36    | level (State (SOME (SkipProof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
    1.37  
    1.38  fun str_of_state (State (NONE, _)) = "at top level"
    1.39 @@ -184,7 +184,7 @@
    1.40  
    1.41  fun proof_position_of state =
    1.42    (case node_of state of
    1.43 -    Proof (prf, _) => ProofNode.position prf
    1.44 +    Proof (prf, _) => Proof_Node.position prf
    1.45    | _ => raise UNDEF);
    1.46  
    1.47  val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
    1.48 @@ -207,7 +207,7 @@
    1.49      NONE => []
    1.50    | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
    1.51    | SOME (Proof (prf, _)) =>
    1.52 -      Proof.pretty_state (ProofNode.position prf) (ProofNode.current prf)
    1.53 +      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
    1.54    | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
    1.55    |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
    1.56  
    1.57 @@ -450,7 +450,7 @@
    1.58  
    1.59  fun end_proof f = transaction (fn int =>
    1.60    (fn Proof (prf, (finish, _)) =>
    1.61 -        let val state = ProofNode.current prf in
    1.62 +        let val state = Proof_Node.current prf in
    1.63            if can (Proof.assert_bottom true) state then
    1.64              let
    1.65                val ctxt' = f int state;
    1.66 @@ -475,7 +475,7 @@
    1.67        else ();
    1.68        if skip andalso not schematic then
    1.69          SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
    1.70 -      else Proof (ProofNode.init prf, (finish gthy, gthy))
    1.71 +      else Proof (Proof_Node.init prf, (finish gthy, gthy))
    1.72      end
    1.73    | _ => raise UNDEF));
    1.74  
    1.75 @@ -499,12 +499,12 @@
    1.76      | _ => raise UNDEF));
    1.77  
    1.78  val present_proof = present_transaction (fn _ =>
    1.79 -  (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
    1.80 +  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
    1.81      | skip as SkipProof _ => skip
    1.82      | _ => raise UNDEF));
    1.83  
    1.84  fun proofs' f = transaction (fn int =>
    1.85 -  (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
    1.86 +  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
    1.87      | skip as SkipProof _ => skip
    1.88      | _ => raise UNDEF));
    1.89  
    1.90 @@ -654,7 +654,7 @@
    1.91              Future.fork_pri ~1 (fn () =>
    1.92                let val (states, result_state) =
    1.93                  (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
    1.94 -                  => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
    1.95 +                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
    1.96                  |> fold_map command_result body_trs
    1.97                  ||> command (end_tr |> set_print false);
    1.98                in (states, presentation_context_of result_state) end))