1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 15 15:59:49 2008 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 15 16:02:07 2008 +0200
     1.3 @@ -119,8 +119,9 @@
     1.4  *}
     1.5  
     1.6  (*<*)
     1.7 +setup {*
     1.8 +let
     1.9  
    1.10 -ML {*
    1.11  fun remove_suc thy thms =
    1.12    let
    1.13      val vname = Name.variant (map fst
    1.14 @@ -159,8 +160,7 @@
    1.15                let val (ths1, ths2) = split_list thps
    1.16                in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
    1.17        end
    1.18 -  in
    1.19 -    case get_first mk_thms eqs of
    1.20 +  in case get_first mk_thms eqs of
    1.21        NONE => thms
    1.22      | SOME x => remove_suc thy x
    1.23    end;
    1.24 @@ -215,24 +215,31 @@
    1.25      then remove_suc_clause thy ths else ths
    1.26    end;
    1.27  
    1.28 -fun lift_obj_eq f thy thms =
    1.29 -  thms
    1.30 -  |> try (
    1.31 -    map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    1.32 -    #> f thy
    1.33 -    #> map (fn thm => thm RS @{thm eq_reflection})
    1.34 -    #> map (Conv.fconv_rule Drule.beta_eta_conversion))
    1.35 -  |> the_default thms
    1.36 -*}
    1.37 +fun lift f thy thms1 =
    1.38 +  let
    1.39 +    val thms2 = Drule.zero_var_indexes_list thms1;
    1.40 +    val thms3 = try (map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    1.41 +      #> f thy
    1.42 +      #> map (fn thm => thm RS @{thm eq_reflection})
    1.43 +      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) thms2;
    1.44 +    val thms4 = Option.map Drule.zero_var_indexes_list thms3;
    1.45 +  in case thms4
    1.46 +   of NONE => NONE
    1.47 +    | SOME thms4 => if Thm.eq_thms (thms2, thms4) then NONE else SOME thms4
    1.48 +  end
    1.49  
    1.50 -setup {*
    1.51 +in
    1.52 +
    1.53    Codegen.add_preprocessor eqn_suc_preproc
    1.54    #> Codegen.add_preprocessor clause_suc_preproc
    1.55 -  #> Code.add_functrans ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
    1.56 -  #> Code.add_functrans ("clause_Suc", lift_obj_eq clause_suc_preproc)
    1.57 +  #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
    1.58 +  #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
    1.59 +
    1.60 +end;
    1.61  *}
    1.62  (*>*)
    1.63  
    1.64 +
    1.65  subsection {* Target language setup *}
    1.66  
    1.67  text {*