node_cases renamed to node_case;
authorwenzelm
Mon May 17 21:32:51 1999 +0200 (1999-05-17 ago)
changeset 6662e53968c1df53
parent 6661 24185f54f177
child 6663 3f87294c8704
node_cases renamed to node_case;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon May 17 21:32:08 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 17 21:32:51 1999 +0200
     1.3 @@ -106,9 +106,9 @@
     1.4  fun print_thms (name, srcs) = Toplevel.keep (fn state =>
     1.5    let
     1.6      val ths = map (Thm.transfer (Toplevel.theory_of state))
     1.7 -      (Toplevel.node_cases PureThy.get_thms (ProofContext.get_thms o Proof.context_of)
     1.8 +      (Toplevel.node_case PureThy.get_thms (ProofContext.get_thms o Proof.context_of)
     1.9          state name);
    1.10 -    val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs;
    1.11 +    val ths' = Toplevel.node_case global_attribs local_attribs state ths srcs;
    1.12    in Display.print_thms ths' end);
    1.13  
    1.14  
    1.15 @@ -123,13 +123,13 @@
    1.16  fun print_type s = Toplevel.keep (fn state =>
    1.17    let
    1.18      val sign = Toplevel.sign_of state;
    1.19 -    val T = Toplevel.node_cases read_typ (ProofContext.read_typ o Proof.context_of) state s;
    1.20 +    val T = Toplevel.node_case read_typ (ProofContext.read_typ o Proof.context_of) state s;
    1.21    in Pretty.writeln (Pretty.quote (Sign.pretty_typ sign T)) end);
    1.22  
    1.23  fun print_term s = Toplevel.keep (fn state =>
    1.24    let
    1.25      val sign = Toplevel.sign_of state;
    1.26 -    val t = Toplevel.node_cases (read_term (TVar (("'z", 0), logicS)))
    1.27 +    val t = Toplevel.node_case (read_term (TVar (("'z", 0), logicS)))
    1.28        (ProofContext.read_term o Proof.context_of) state s;
    1.29      val T = Term.type_of t;
    1.30    in
    1.31 @@ -141,7 +141,7 @@
    1.32    let
    1.33      val sign = Toplevel.sign_of state;
    1.34      val prop =
    1.35 -      Toplevel.node_cases (read_term propT) (ProofContext.read_prop o Proof.context_of) state s;
    1.36 +      Toplevel.node_case (read_term propT) (ProofContext.read_prop o Proof.context_of) state s;
    1.37    in Pretty.writeln (Pretty.quote (Sign.pretty_term sign prop)) end);
    1.38  
    1.39