src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 43294 0271fda2a83a
parent 43268 c0eaa8b9bff5
child 43297 e77baf329f48
equal deleted inserted replaced
43293:a80cdc4b27a3 43294:0271fda2a83a
   228   | simp_not_not t = t
   228   | simp_not_not t = t
   229 
   229 
   230 (* Match untyped terms. *)
   230 (* Match untyped terms. *)
   231 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
   231 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
   232   | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
   232   | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
   233   | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b)
   233   | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) =
       
   234     (a = b) (* ignore variable numbers *)
   234   | untyped_aconv (Bound i, Bound j) = (i = j)
   235   | untyped_aconv (Bound i, Bound j) = (i = j)
   235   | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
   236   | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
   236   | untyped_aconv (t1 $ t2, u1 $ u2) =
   237   | untyped_aconv (t1 $ t2, u1 $ u2) =
   237     untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
   238     untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
   238   | untyped_aconv _ = false
   239   | untyped_aconv _ = false