src/HOL/Product_Type.thy
changeset 13480 bb72bd43c6c3
parent 13462 56610e2ba220
child 14101 d25c23e46173
     1.1 --- a/src/HOL/Product_Type.thy	Thu Aug 08 23:42:49 2002 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Aug 08 23:46:09 2002 +0200
     1.3 @@ -336,9 +336,9 @@
     1.4    fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
     1.5    |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
     1.6    |   split_pat tp i _ = None;
     1.7 -  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
     1.8 -        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
     1.9 -        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
    1.10 +  fun metaeq sg lhs rhs = mk_meta_eq (Tactic.prove sg [] []
    1.11 +        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    1.12 +        (K (simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1)));
    1.13  
    1.14    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    1.15    |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse