equal
deleted
inserted
replaced
149 end; |
149 end; |
150 in |
150 in |
151 thy |
151 thy |
152 |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) |
152 |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) |
153 |> PrimrecPackage.add_primrec |
153 |> PrimrecPackage.add_primrec |
154 [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] |
154 [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] |
155 (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs') |
155 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs') |
156 |-> add_code |
156 |-> add_code |
157 |> `(fn lthy => Syntax.check_term lthy eq) |
157 |> `(fn lthy => Syntax.check_term lthy eq) |
158 |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) |
158 |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) |
159 |> snd |
159 |> snd |
160 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
160 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
161 |> LocalTheory.exit_global |
161 |> LocalTheory.exit_global |
162 end |
162 end |
163 | random_inst tycos thy = raise REC |
163 | random_inst tycos thy = raise REC |