1.1 --- a/src/Pure/Isar/obtain.ML	Thu Feb 01 20:44:19 2001 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Feb 01 20:45:11 2001 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5    {
     1.6      fix thesis
     1.7 -    assume that: "!!x. P x ==> thesis"
     1.8 +    assume that [intro]: "!!x. P x ==> thesis"
     1.9      <chain_facts> have thesis <proof (insert that)>
    1.10    }
    1.11    fix x assm (obtained) "P x"