src/HOL/Tools/specification_package.ML
changeset 18776 fdc5379fd359
parent 18729 216e31270509
child 18799 f137c5e971f5
equal deleted inserted replaced
18775:becdbf57eeb8 18776:fdc5379fd359
   124           | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
   124           | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
   125 
   125 
   126         fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (u,t);
   126         fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (u,t);
   127 
   127 
   128         val rew_imps = alt_props |>
   128         val rew_imps = alt_props |>
   129           map (ObjectLogic.atomize_cterm thy o Thm.read_cterm thy o rpair Term.propT o snd)
   129           map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd)
   130         val props' = rew_imps |>
   130         val props' = rew_imps |>
   131           map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of)
   131           map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of)
   132 
   132 
   133         fun proc_single prop =
   133         fun proc_single prop =
   134             let
   134             let