src/Pure/meta_simplifier.ML
changeset 13614 0b91269c0b13
parent 13607 6908230623a3
child 13661 ec97dfc2bfe0
equal deleted inserted replaced
13613:531f1f524848 13614:0b91269c0b13
   740              in case botc skel' mss' t' of
   740              in case botc skel' mss' t' of
   741                   Some thm => Some (abstract_rule a v thm)
   741                   Some thm => Some (abstract_rule a v thm)
   742                 | None => None
   742                 | None => None
   743              end
   743              end
   744          | t $ _ => (case t of
   744          | t $ _ => (case t of
   745              Const ("==>", _) $ _  =>
   745              Const ("==>", _) $ _  => impc t0 mss
   746                let val (s, u) = Drule.dest_implies t0
       
   747                in impc t0 mss end
       
   748            | Abs _ =>
   746            | Abs _ =>
   749                let val thm = beta_conversion false t0
   747                let val thm = beta_conversion false t0
   750                in case subc skel0 mss (rhs_of thm) of
   748                in case subc skel0 mss (rhs_of thm) of
   751                     None => Some thm
   749                     None => Some thm
   752                   | Some thm' => Some (transitive thm thm')
   750                   | Some thm' => Some (transitive thm thm')