src/FOL/simpdata.ML
changeset 6391 0da748358eff
parent 6114 45958e54d72e
child 7355 4c43090659ca
     1.1 --- a/src/FOL/simpdata.ML	Wed Mar 17 16:33:00 1999 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Mar 17 16:33:47 1999 +0100
     1.3 @@ -243,10 +243,10 @@
     1.4  
     1.5  local
     1.6  val ex_pattern =
     1.7 -  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
     1.8 +  read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
     1.9  
    1.10  val all_pattern =
    1.11 -  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    1.12 +  read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    1.13  
    1.14  in
    1.15  val defEX_regroup =