src/Pure/Isar/isar_thy.ML
changeset 7176 a329a37ed91a
parent 7172 9ecd66cf546d
child 7242 f17f2e8ba0c7
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Aug 04 18:20:24 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Aug 05 22:08:53 1999 +0200
     1.3 @@ -295,14 +295,14 @@
     1.4  val presume_i   = local_statement_i Proof.presume_i I o Comment.ignore;
     1.5  val local_def   = local_statement LocalDefs.def I o Comment.ignore;
     1.6  val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore;
     1.7 -val show        = local_statement Proof.show I o Comment.ignore;
     1.8 -val show_i      = local_statement_i Proof.show_i I o Comment.ignore;
     1.9 -val have        = local_statement Proof.have I o Comment.ignore;
    1.10 -val have_i      = local_statement_i Proof.have_i I o Comment.ignore;
    1.11 -val thus        = local_statement Proof.show Proof.chain o Comment.ignore;
    1.12 -val thus_i      = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
    1.13 -val hence       = local_statement Proof.have Proof.chain o Comment.ignore;
    1.14 -val hence_i     = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
    1.15 +val show        = local_statement (Proof.show Seq.single) I o Comment.ignore;
    1.16 +val show_i      = local_statement_i (Proof.show_i Seq.single) I o Comment.ignore;
    1.17 +val have        = local_statement (Proof.have Seq.single) I o Comment.ignore;
    1.18 +val have_i      = local_statement_i (Proof.have_i Seq.single) I o Comment.ignore;
    1.19 +val thus        = local_statement (Proof.show Seq.single) Proof.chain o Comment.ignore;
    1.20 +val thus_i      = local_statement_i (Proof.show_i Seq.single) Proof.chain o Comment.ignore;
    1.21 +val hence       = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore;
    1.22 +val hence_i     = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore;
    1.23  
    1.24  
    1.25  (* blocks *)