Fixed problem with patterns in lambdas
authornipkow
Tue Jul 03 15:23:11 2007 +0200 (2007-07-03)
changeset 23529958f9d9cfb63
parent 23528 55597852285a
child 23530 438c5d2db482
Fixed problem with patterns in lambdas
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Tue Jul 03 14:48:27 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jul 03 15:23:11 2007 +0200
     1.3 @@ -132,24 +132,19 @@
     1.4  text{* Lambda-abstractions with pattern matching: *}
     1.5  
     1.6  syntax
     1.7 -  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(%_)" 10)
     1.8 +  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
     1.9  syntax (xsymbols)
    1.10 -  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
    1.11 +  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
    1.12  
    1.13 -ML{*
    1.14 -local
    1.15 -fun fun_tr ctxt [cs] =
    1.16 -  let val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
    1.17 -                 [Bound 0,cs]
    1.18 -  in Abs("", dummyT, ft) end;
    1.19 -in
    1.20 -val trfun_setup =
    1.21 -  Theory.add_advanced_trfuns ([],
    1.22 -    [("_fun_syntax", fun_tr)],
    1.23 -    [], []);
    1.24 -end
    1.25 +parse_translation (advanced) {*
    1.26 +let
    1.27 +  fun fun_tr ctxt [cs] =
    1.28 +    let
    1.29 +      val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
    1.30 +      val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
    1.31 +                 [x, cs]
    1.32 +    in lambda x ft end
    1.33 +in [("_lam_pats_syntax", fun_tr)] end
    1.34  *}
    1.35  
    1.36 -setup trfun_setup
    1.37 -
    1.38  end