src/HOL/Tools/function_package/pattern_split.ML
changeset 20654 d80502f0d701
parent 20636 ddddf0b7d322
child 21051 c49467a9c1e1
     1.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Thu Sep 21 03:17:51 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Thu Sep 21 12:22:05 2006 +0200
     1.3 @@ -94,9 +94,6 @@
     1.4        val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
     1.5        val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
     1.6  
     1.7 -      val _ = print (cterm_of thy eq1)
     1.8 -      val _ = print (cterm_of thy eq2)
     1.9 -
    1.10        val substs = pattern_subtract_subst ctx vs lhs1 lhs2
    1.11  
    1.12        fun instantiate (vs', sigma) =
    1.13 @@ -105,10 +102,8 @@
    1.14            in
    1.15              fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
    1.16            end
    1.17 -
    1.18 -      fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
    1.19      in
    1.20 -      prtrm (map instantiate substs)
    1.21 +      map instantiate substs
    1.22      end
    1.23  
    1.24