equal
deleted
inserted
replaced
105 of NONE => ([], x) |
105 of NONE => ([], x) |
106 | SOME (x1, x2) => |
106 | SOME (x1, x2) => |
107 let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; |
107 let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; |
108 |
108 |
109 |
109 |
110 (** language core - types, pattern, expressions **) |
110 (** language core - types, patterns, expressions **) |
111 |
111 |
112 (* language representation *) |
112 (* language representation *) |
113 |
113 |
114 type vname = string; |
114 type vname = string; |
115 |
115 |
478 fun stmt_classparam class = |
478 fun stmt_classparam class = |
479 ensure_class thy algbr funcgr class |
479 ensure_class thy algbr funcgr class |
480 #>> Classparam; |
480 #>> Classparam; |
481 fun stmt_fun trns = |
481 fun stmt_fun trns = |
482 let |
482 let |
483 val raw_thms = Code_Funcgr.funcs funcgr c; |
483 val raw_thms = Code_Funcgr.eqns funcgr c; |
484 val (vs, raw_ty) = Code_Funcgr.typ funcgr c; |
484 val (vs, raw_ty) = Code_Funcgr.typ funcgr c; |
485 val ty = Logic.unvarifyT raw_ty; |
485 val ty = Logic.unvarifyT raw_ty; |
486 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty |
486 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty |
487 then raw_thms |
487 then raw_thms |
488 else (map o apfst) (Code_Unit.expand_eta 1) raw_thms; |
488 else (map o apfst) (Code_Unit.expand_eta 1) raw_thms; |