1.1 --- a/src/HOL/Rat.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -1171,6 +1171,21 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation rat :: partial_term_of
     1.8 +begin
     1.9 +
    1.10 +instance ..
    1.11 +
    1.12 +end
    1.13 +
    1.14 +lemma [code]:
    1.15 +  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
    1.16 +  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
    1.17 +     Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Fract'')
    1.18 +     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [],
    1.19 +        Typerep.Typerep (STR ''Rat.rat'') []]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k)" 
    1.20 +by (rule partial_term_of_anything)+
    1.21 +
    1.22  instantiation rat :: narrowing
    1.23  begin
    1.24