src/HOL/simpdata.ML
changeset 6394 3d9fd50fcc43
parent 6301 08245f5a436d
child 6514 381fb2b084a4
     1.1 --- a/src/HOL/simpdata.ML	Wed Mar 17 16:53:32 1999 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Mar 17 16:53:46 1999 +0100
     1.3 @@ -315,10 +315,10 @@
     1.4  
     1.5  local
     1.6  val ex_pattern =
     1.7 -  read_cterm (sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
     1.8 +  Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
     1.9  
    1.10  val all_pattern =
    1.11 -  read_cterm (sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.12 +  Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.13  
    1.14  in
    1.15  val defEX_regroup =