equal
deleted
inserted
replaced
13 struct |
13 struct |
14 |
14 |
15 |
15 |
16 (* nibble *) |
16 (* nibble *) |
17 |
17 |
|
18 val nib_prefix = "String.nibble."; |
|
19 |
18 val mk_nib = |
20 val mk_nib = |
19 Syntax.Constant o unprefix "List.nibble." o |
21 Syntax.Constant o unprefix nib_prefix o |
20 fst o Term.dest_Const o HOLogic.mk_nibble; |
22 fst o Term.dest_Const o HOLogic.mk_nibble; |
21 |
23 |
22 fun dest_nib (Syntax.Constant c) = |
24 fun dest_nib (Syntax.Constant c) = |
23 HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT)) |
25 HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT)) |
24 handle TERM _ => raise Match; |
26 handle TERM _ => raise Match; |
25 |
27 |
26 |
28 |
27 (* char *) |
29 (* char *) |
28 |
30 |