src/ZF/constructor.ML
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 1103 08fda5148971
     1.1 --- a/src/ZF/constructor.ML	Thu Aug 18 12:56:57 1994 +0200
     1.2 +++ b/src/ZF/constructor.ML	Thu Aug 18 17:41:40 1994 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  (*Get the case term from its definition*)
     1.6  val Const("==",_) $ big_case_tm $ _ =
     1.7 -    hd con_defs |> rep_thm |> #prop |> unvarify;
     1.8 +    hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
     1.9  
    1.10  val (_, big_case_args) = strip_comb big_case_tm;
    1.11  
    1.12 @@ -62,8 +62,9 @@
    1.13  			Su.case_inr RS trans] 1)];
    1.14  
    1.15  fun prove_case_equation (arg,con_def) =
    1.16 -    prove_term (sign_of thy) [] 
    1.17 -        (mk_case_equation arg, case_tacsf con_def);
    1.18 +    prove_goalw_cterm [] 
    1.19 +        (cterm_of (sign_of thy) (mk_case_equation arg))
    1.20 +	(case_tacsf con_def);
    1.21  
    1.22  val free_iffs = 
    1.23      map standard (con_defs RL [def_swap_iff]) @