equal
deleted
inserted
replaced
405 val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; |
405 val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; |
406 val case2 = |
406 val case2 = |
407 Syntax.const @{syntax_const "_case1"} $ |
407 Syntax.const @{syntax_const "_case1"} $ |
408 Syntax.const @{const_syntax dummy_pattern} $ NilC; |
408 Syntax.const @{const_syntax dummy_pattern} $ NilC; |
409 val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; |
409 val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; |
410 in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end; |
410 in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr ctxt [x, cs]] end; |
411 |
411 |
412 fun abs_tr ctxt p e opti = |
412 fun abs_tr ctxt p e opti = |
413 (case Term_Position.strip_positions p of |
413 (case Term_Position.strip_positions p of |
414 Free (s, T) => |
414 Free (s, T) => |
415 let |
415 let |