[isabelle] Exception using setup_lifting



Hello,

I'm currently exploring several graph representations and encountered an unexpected exception using the lifting package. The following code:
```
type_synonym 'i graph_rep = "'i fset × 'i fset × ('i,'i) fmap × ('i,'i) fmap"

typedef 'i graph =
  "{(nodes, edges, src, trg) :: 'i graph_rep |
      nodes edges src trg.
  fmdom src |⊆| edges ∧ fmran src |⊆| nodes ∧ fmdom trg |⊆| edges ∧ fmran trg |⊆| nodes
  }"
  apply (rule exI[where x = "(fempty, fempty, fmempty, fmempty)"])
  by simp

setup_lifting type_definition_graph
```

produces the exception:
```
exception THM 1 raised (line 1828 of "thm.ML"):
  dest_state
  Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T)  [Quotient R Abs Rep T]
```

Would be great to receive some comments and potential suggestions on how to overcome this issue.

Thank you in advance,
Robert




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.