20 val name: morphism > string > string 
20 val name: morphism > string > string 
21 val typ: morphism > typ > typ 
21 val typ: morphism > typ > typ 
22 val term: morphism > term > term 
22 val term: morphism > term > term 
23 val fact: morphism > thm list > thm list 
23 val fact: morphism > thm list > thm list 
24 val thm: morphism > thm > thm 
24 val thm: morphism > thm > thm 

25 val cterm: morphism > cterm > cterm 
25 val morphism: 
26 val morphism: 
26 {name: string > string, 
27 {name: string > string, 
27 var: string * mixfix > string * mixfix, 
28 var: string * mixfix > string * mixfix, 
28 typ: typ > typ, 
29 typ: typ > typ, 
29 term: term > term, 
30 term: term > term, 
52 fun var (Morphism {var, ...}) = var; 
53 fun var (Morphism {var, ...}) = var; 
53 fun typ (Morphism {typ, ...}) = typ; 
54 fun typ (Morphism {typ, ...}) = typ; 
54 fun term (Morphism {term, ...}) = term; 
55 fun term (Morphism {term, ...}) = term; 
55 fun fact (Morphism {fact, ...}) = fact; 
56 fun fact (Morphism {fact, ...}) = fact; 
56 val thm = singleton o fact; 
57 val thm = singleton o fact; 

58 val cterm = Drule.cterm_rule o thm; 
57 
59 
58 val morphism = Morphism; 
60 val morphism = Morphism; 
59 
61 
60 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I}; 
62 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I}; 
61 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I}; 
63 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I}; 