src/Pure/Isar/obtain.ML
changeset 12055 a9c44895cc8c
parent 11890 28e42a90bea8
child 12145 c38a7efa3afb
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Nov 05 20:58:28 2001 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Nov 05 20:59:35 2001 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    in
     1.5      if not (null bads) then
     1.6        raise Proof.STATE ("Conclusion contains obtained parameters: " ^
     1.7 -        space_implode " " (map (Sign.string_of_term sign) bads), state)
     1.8 +        space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
     1.9      else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
    1.10        raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    1.11      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule